Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 28-Apr-2017 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.
(13-Apr-2017) See equidK for a discussion of the recent theorems in my mathbox. -NM
(24-Mar-2017) Alan Sare updated his completeusersproof program.
(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.
(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).
(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.
(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.
(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.
(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.
(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.
(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.
(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").
(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.
(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.
(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica
(12-Aug-2016) A Gitter chat room has been created for Metamath.
(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project
(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.
(4-Aug-2016) Mario gave two presentations at CICM 2016.
(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.
(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.
(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.
(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.
(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).
(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language. Older news...
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
23-Apr-2017 | ax9dgenK 27911 | Degenerate case of ax-9 1684. Uses only Tarski's FOL axiom schemes (see description for equidK 27889). (Contributed by NM, 23-Apr-2017.) |
20-Apr-2017 | stowei 26947 | This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 26946: often times it will be better to use stoweid 26946 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweid 26946 | This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem62 26945 | This theorem proves the Stone Weierstrass theorem for the non trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem61 26944 | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 92: is in the subalgebra, and for all in , abs( f(t) - g(t) ) < 2*ε. Here is used to represent f in the paper, and is used to represent ε. For this lemma there's the further assumption that the function to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem60 26943 | This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all in , there is a such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here is used to represent f in the paper, and is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem59 26942 | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: x_{j} is in the subalgebra, 0 <= x_{j} <= 1, x_{j} < ε / n on A_{j} (meaning A in the paper), x_{j} > 1 - \epslon / n on B_{j}. Here is used to represent A in the paper (because A is used for the subalgebra of functions), is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem58 26941 | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem57 26940 | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem56 26939 | This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here is used to represent t_{0} in the paper, is used to represent in the paper, and is used to represent ε (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem55 26938 | This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Here Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem54 26937 | There exists a function as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem53 26936 | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem52 26935 | There exists a neighborood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t_{0} in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem51 26934 | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem50 26933 | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem49 26932 | There exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on , and q_{n} > 1 - ε on . Here y is used to represent the final q_{n} in the paper (the one with n large enough), represents in the paper, represents , represents δ, represents ε, and represents . (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem48 26931 | This lemma is used to prove that built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < ε on . Here is used to represent in the paper, is used to represent ε in the paper, and is used to represent in the paper (because is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem47 26930 | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem46 26929 | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem45 26928 | This lemma proves that, given an appropriate (in another theorem we prove such a exists), there exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on T \ U, and q_{n} > 1 - ε on . We use y to represent the final q_{n} in the paper (the one with n large enough), to represent in the paper, to represent , to represent δ, to represent ε, and to represent . (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem44 26927 | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem43 26926 | This lemma is used to prove the existence of a function p_{t} as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p_{t} in the subalgebra, such that p_{t}( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. Hera Z is used for t_{0} , S is used for t e. T - U , h is used for p_{t}. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem42 26925 | This lemma is used to prove that built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - ε on B. Here is used to represent in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem41 26924 | This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - q_{n"};. Here is used to represent ε in the paper, and to represent q_{n} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem40 26923 | This lemma proves that q_{n} is in the subalgebra, as in the prove of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent q_{n} in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem39 26922 | This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that is a finite subset of , indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_{i} ≤ 1, x_{i} < ε / m on V(t_{i}), and x_{i} > 1 - ε / m on . Here is used to represent A in the paper's Lemma 2 (because is used for the subalgebra), is used to represent m in the paper, is used to represent ε, and v_{i} is used to represent V(t_{i}). is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem38 26921 | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by GlaucoSiliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem37 26920 | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem36 26919 | This lemma is used to prove the existence of a function p_{t} as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that p_{t} ( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. Z is used for t_{0} , S is used for t e. T - U , h is used for p_{t} . G is used for (h_{t})^2 and the final h is a normalized version of G ( divided by it's norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem35 26918 | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem34 26917 | This lemma proves that for all in there is a as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem33 26916 | If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem32 26915 | If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem31 26914 | This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that is a finite subset of , indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all ranging in the finite indexing set, 0 ≤ x_{i} ≤ 1, x_{i} < ε / m on V(t_{i}), and x_{i} > 1 - ε / m on . Here M is used to represent m in the paper, is used to represent ε in the paper, v_{i} is used to represent V(t_{i}). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem30 26913 | This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem29 26912 | When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem28 26911 | There exists a δ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on . Here is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem27 26910 | This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem26 26909 | This lemma is used to prove that there is a function as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here is used to represnt j in the paper, is used to represent A in the paper, is used to represent t, and is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem25 26908 | This lemma proves that for n sufficiently large, q_{n}( t ) < ε, for all in : see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). is used to represent q_{n} in the paper, to represent n in the paper, to represent k, to represent δ, to represent p, and to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem24 26907 | This lemma proves that for sufficiently large, q_{n}( t ) > ( 1 - epsilon ), for all in : see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). is used to represent q_{n} in the paper, to represent in the paper, to represent , to represent δ, and to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem23 26906 | This lemma is used to prove the existence of a function p_{t} as in the beginning of Lemma 1 [BrosowskiDeutsh] p. 90: for all t in T - U, there exists a function p in the subalgebra, such that p_{t} ( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem22 26905 | If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem21 26904 | Once the Stone Weierstrass theorem has been proven for approximating nonnegative functions, then this lemma is used to extend the result to functions with (possibly) negative values. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem20 26903 | If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem19 26902 | If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem18 26901 | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem17 26900 | This lemma proves that the function (as defined in [BrosowskiDeutsh] p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem16 26899 | Lemma for stoweid 26946. The subset of functions in the algebra , with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem15 26898 | This lemma is used to prove the existence of a function as in Lemma 1 from [BrosowskiDeutsh] p. 90: is in the subalgebra, such that 0 ≤ p ≤ 1, p_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem14 26897 | There exists a as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: is an integer and 1 < k * δ < 2. is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem13 26896 | Lemma for stoweid 26946. This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon , in [BrosowskiDeutsh] p. 92, the last step of the proof. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem12 26895 | Lemma for stoweid 26946. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem11 26894 | This lemma is used to prove that there is a function as in the proof of [BrosowskiDeutsh] p. 92, (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem10 26893 | Lemma for stoweid 26946. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90, this lemma is an application of Bernoulli's inequality. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem9 26892 | Lemma for stoweid 26946: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem8 26891 | Lemma for stoweid 26946: two class variables replace two set variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem7 26890 | This lemma is used to prove that q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that q_{n} < ε on , and q_{n} > 1 - ε on . Here it is proven that, for large enough, 1-(k*δ/2)^n > 1 - ε , and 1/(k*δ)^n < ε. The variable is used to represent (k*δ) in the paper, and is used to represent (k*δ/2). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem6 26889 | Lemma for stoweid 26946: two class variables replace two set variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem5 26888 | There exists a δ as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: 0 < δ < 1 , p >= δ on . Here is used to represent δ in the paper and to represent in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem4 26887 | Lemma for stoweid 26946: a class variable replaces a set variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem3 26886 | Lemma for stoweid 26946: if is positive and all terms of a finite product are larger than , then the finite product is larger than A^M. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem2 26885 | lemma for stoweid 26946: here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | stoweidlem1 26884 | Lemma for stoweid 26946. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 11105. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | fmul01lt1 26883 | Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | fmul01lt1lem2 26882 | Given a finite multiplication of values betweeen 0 and 1, a value larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | fmul01lt1lem1 26881 | Given a finite multiplication of values betweeen 0 and 1, a value larger than its frist element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | fmuldfeq 26880 | X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | fmuldfeqlem1 26879 | induction step for the proof of fmuldfeq 26880. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
20-Apr-2017 | fmulcl 26878 | If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |