Home | Metamath
Proof Explorer Theorem List (p. 375 of 393) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-26406) |
Hilbert Space Explorer
(26407-27929) |
Users' Mathboxes
(27930-39300) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itgeq1d 37401* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | mbf0 37402 | The empty set is a measurable function (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
MblFn | ||
Theorem | mbfres2cn 37403 | Measurability of a piecewise function: if is measurable on subsets and of its domain, and these pieces make up all of , then is measurable on the whole domain. Similar to mbfres2 22478 but here the theorem is extended to complex valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
MblFn MblFn MblFn | ||
Theorem | vol0 37404 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ditgeqiooicc 37405* | A function on an open interval, has the same directed integral as its extension on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
_ _ | ||
Theorem | volge0 37406 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | cnbdibl 37407* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | snmbl 37408 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ditgeq3d 37409* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
_ _ | ||
Theorem | iblempty 37410 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | iblsplit 37411* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | volsn 37412 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | itgvol0 37413* | If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | itgcoscmulx 37414* | Exercise: the integral of on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | iblsplitf 37415* | A version of iblsplit 37411 using bound-variable hypotheses instead of distinct variable conditions" (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ibliooicc 37416* | If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | volioc 37417 | The measure of left open, right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | iblspltprt 37418* | If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | itgsincmulx 37419* | Exercise: the integral of on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | itgsubsticclem 37420* | lemma for itgsubsticc 37421 (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
_ _ | ||
Theorem | itgsubsticc 37421* | Integration by u-substitution. The main difference with respect to itgsubst 22878 is that here we consider the range of to be in the closed interval . If is a continuous, differentiable function from to , whose derivative is continuous and integrable, and is a continuous function on , then the integral of from to is equal to the integral of from to . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
_ _ | ||
Theorem | itgioocnicc 37422* | The integral of a piecewise continuous function on an open interval is equal to the integral of the continuous function , in the corresponding closed interval. is equal to on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim lim | ||
Theorem | iblcncfioo 37423 | A continuous function on an open interval with a finite right limit in and a finite left limit in is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim lim | ||
Theorem | itgspltprt 37424* | The integral splits on a given partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ | ||
Theorem | itgiccshift 37425* | The integral of a function, stays the same if its closed interval domain is shifted by . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | itgperiod 37426* | The integral of a periodic function, with period stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | itgsbtaddcnst 37427* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
_ _ | ||
Theorem | itgeq2d 37428* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | stoweidlem1 37429 | Lemma for stoweid 37493. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12395. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem2 37430* | lemma for stoweid 37493: here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem3 37431* | Lemma for stoweid 37493: 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.) |
Theorem | stoweidlem4 37432* | Lemma for stoweid 37493: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem5 37433* | 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.) |
Theorem | stoweidlem6 37434* | Lemma for stoweid 37493: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem7 37435* | 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.) |
Theorem | stoweidlem8 37436* | Lemma for stoweid 37493: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem9 37437* | Lemma for stoweid 37493: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem10 37438 | Lemma for stoweid 37493. 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.) |
Theorem | stoweidlem11 37439* | 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.) |
Theorem | stoweidlem12 37440* | Lemma for stoweid 37493. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem13 37441 | Lemma for stoweid 37493. This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon, in the last step of the proof in [BrosowskiDeutsh] p. 92. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem14 37442* | 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.) |
Theorem | stoweidlem15 37443* | 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.) |
Theorem | stoweidlem16 37444* | Lemma for stoweid 37493. The subset of functions in the algebra , with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem17 37445* | 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.) |
Theorem | stoweidlem18 37446* | 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.) |
Theorem | stoweidlem19 37447* | 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.) |
Theorem | stoweidlem20 37448* | 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.) |
Theorem | stoweidlem21 37449* | 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.) |
Theorem | stoweidlem22 37450* | 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.) |
Theorem | stoweidlem23 37451* | 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.) |
Theorem | stoweidlem24 37452* | 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.) |
Theorem | stoweidlem25 37453* | 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.) |
Theorem | stoweidlem26 37454* | 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.) |
Theorem | stoweidlem27 37455* | 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.) |
Theorem | stoweidlem28 37456* | 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.) |
Theorem | stoweidlem29 37457* | 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.) (Revised by AV, 13-Sep-2020.) |
inf inf inf | ||
Theorem | stoweidlem29OLD 37458* | 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.) Obsolete version of stoweidlem29 37457 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | stoweidlem30 37459* | 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.) |
Theorem | stoweidlem31 37460* | 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.) |
Theorem | stoweidlem32 37461* | 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.) |
Theorem | stoweidlem33 37462* | 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.) |
Theorem | stoweidlem34 37463* | 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.) |
Theorem | stoweidlem35 37464* | 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.) |
Theorem | stoweidlem36 37465* | 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 its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem37 37466* | 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.) |
Theorem | stoweidlem38 37467* | 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.) |
Theorem | stoweidlem39 37468* | 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.) |
Theorem | stoweidlem40 37469* | This lemma proves that q_{n} is in the subalgebra, as in the proof 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.) |
Theorem | stoweidlem41 37470* | 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.) |
Theorem | stoweidlem42 37471* | 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.) |
Theorem | stoweidlem43 37472* | 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.) |
Theorem | stoweidlem44 37473* | 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.) |
Theorem | stoweidlem45 37474* | 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.) |
Theorem | stoweidlem46 37475* | 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.) |
Theorem | stoweidlem47 37476* | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem48 37477* | 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.) |
Theorem | stoweidlem49 37478* | 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.) |
Theorem | stoweidlem50 37479* | 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.) |
Theorem | stoweidlem51 37480* | 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.) |
Theorem | stoweidlem52 37481* | 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.) |
Theorem | stoweidlem53 37482* | 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.) |
Theorem | stoweidlem54 37483* | 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.) |
Theorem | stoweidlem55 37484* | 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.) |
Theorem | stoweidlem56 37485* | 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.) |
Theorem | stoweidlem57 37486* | 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.) |
Theorem | stoweidlem58 37487* | 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.) |
Theorem | stoweidlem59 37488* | 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.) |
Theorem | stoweidlem60 37489* | 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.) |