Home | Metamath
Proof Explorer Theorem List (p. 440 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itgsin0pilem1 43901* | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΆ = (π‘ β (0[,]Ο) β¦ -(cosβπ‘)) β β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | ibliccsinexp 43902* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄[,]π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsin0pi 43903 | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | iblioosinexp 43904* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄(,)π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsinexplem1 43905* | Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π₯ β β β¦ ((sinβπ₯)βπ)) & β’ πΊ = (π₯ β β β¦ -(cosβπ₯)) & β’ π» = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯))) & β’ πΌ = (π₯ β β β¦ (((sinβπ₯)βπ) Β· (sinβπ₯))) & β’ πΏ = (π₯ β β β¦ (((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)) Β· -(cosβπ₯))) & β’ π = (π₯ β β β¦ (((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1)))) & β’ (π β π β β) β β’ (π β β«(0(,)Ο)(((sinβπ₯)βπ) Β· (sinβπ₯)) dπ₯ = (π Β· β«(0(,)Ο)(((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1))) dπ₯)) | ||
Theorem | itgsinexp 43906* | A recursive formula for the integral of sin^N on the interval (0,Ο) . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β (β€β₯β2)) β β’ (π β (πΌβπ) = (((π β 1) / π) Β· (πΌβ(π β 2)))) | ||
Theorem | iblconstmpt 43907* | A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β dom vol β§ (volβπ΄) β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β πΏ1) | ||
Theorem | itgeq1d 43908* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ = π΅) β β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | mbfres2cn 43909 | 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 24931 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β (πΉ βΎ π΅) β MblFn) & β’ (π β (πΉ βΎ πΆ) β MblFn) & β’ (π β (π΅ βͺ πΆ) = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | vol0 43910 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (volββ ) = 0 | ||
Theorem | ditgeqiooicc 43911* | 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.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) β β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β¨[π΄ β π΅](πΊβπ₯) dπ₯) | ||
Theorem | volge0 43912 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β dom vol β 0 β€ (volβπ΄)) | ||
Theorem | cnbdibl 43913* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β dom vol) & β’ (π β (volβπ΄) β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | snmbl 43914 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β {π΄} β dom vol) | ||
Theorem | ditgeq3d 43915* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β€ π΅) & β’ ((π β§ π₯ β (π΄(,)π΅)) β π· = πΈ) β β’ (π β β¨[π΄ β π΅]π· dπ₯ = β¨[π΄ β π΅]πΈ dπ₯) | ||
Theorem | iblempty 43916 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β πΏ1 | ||
Theorem | iblsplit 43917* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | volsn 43918 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (volβ{π΄}) = 0) | ||
Theorem | itgvol0 43919* | If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β§ β«π΄π΅ dπ₯ = 0)) | ||
Theorem | itgcoscmulx 43920* | Exercise: the integral of π₯ β¦ cosππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) & β’ (π β π΄ β 0) β β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) | ||
Theorem | iblsplitf 43921* | A version of iblsplit 43917 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | ibliooicc 43922* | If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π₯ β (π΄(,)π΅) β¦ πΆ) β πΏ1) & β’ ((π β§ π₯ β (π΄[,]π΅)) β πΆ β β) β β’ (π β (π₯ β (π΄[,]π΅) β¦ πΆ) β πΏ1) | ||
Theorem | volioc 43923 | The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,]π΅)) = (π΅ β π΄)) | ||
Theorem | iblspltprt 43924* | 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.) |
β’ β²π‘π & β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ ((π β§ π β (π...π)) β (πβπ) β β) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β (π‘ β ((πβπ)[,](πβπ)) β¦ π΄) β πΏ1) | ||
Theorem | itgsincmulx 43925* | Exercise: the integral of π₯ β¦ sinππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) β β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) | ||
Theorem | itgsubsticclem 43926* | lemma for itgsubsticc 43927. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π’ β (πΎ[,]πΏ) β¦ πΆ) & β’ πΊ = (π’ β β β¦ if(π’ β (πΎ[,]πΏ), (πΉβπ’), if(π’ < πΎ, (πΉβπΎ), (πΉβπΏ)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β πΉ β ((πΎ[,]πΏ)βcnββ)) & β’ (π β πΎ β β) & β’ (π β πΏ β β) & β’ (π β πΎ β€ πΏ) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubsticc 43927* | Integration by u-substitution. The main difference with respect to itgsubst 25335 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 πΆ(π΄(π₯)) D π΄(π₯) from π to π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π’ β (πΎ[,]πΏ) β¦ πΆ) β ((πΎ[,]πΏ)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) & β’ (π β πΎ β β) & β’ (π β πΏ β β) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgioocnicc 43928* | 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.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β (πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) & β’ (π β (π΄[,]π΅) β dom πΉ) & β’ (π β π β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) & β’ (π β πΏ β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) β β’ (π β (πΊ β πΏ1 β§ β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯)) | ||
Theorem | iblcncfioo 43929 | 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.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΉ β πΏ1) | ||
Theorem | itgspltprt 43930* | The β« integral splits on a given partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π:(π...π)βΆβ) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β β«((πβπ)[,](πβπ))π΄ dπ‘ = Ξ£π β (π..^π)β«((πβπ)[,](πβ(π + 1)))π΄ dπ‘) | ||
Theorem | itgiccshift 43931* | The integral of a function, πΉ stays the same if its closed interval domain is shifted by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β π β β+) & β’ πΊ = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgperiod 43932* | 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.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β+) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgsbtaddcnst 43933* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β¨[(π΄ β π) β (π΅ β π)](πΉβ(π + π )) dπ = β¨[π΄ β π΅](πΉβπ‘) dπ‘) | ||
Theorem | volico 43934 | The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) = if(π΄ < π΅, (π΅ β π΄), 0)) | ||
Theorem | sublevolico 43935 | The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΅ β π΄) β€ (volβ(π΄[,)π΅))) | ||
Theorem | dmvolss 43936 | Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β π« β | ||
Theorem | ismbl3 43937* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl2 24813, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))) β€ (vol*βπ₯))) | ||
Theorem | volioof 43938 | The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (vol β (,)):(β* Γ β*)βΆ(0[,]+β) | ||
Theorem | ovolsplit 43939 | The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) β β’ (π β (vol*βπ΄) β€ ((vol*β(π΄ β© π΅)) +π (vol*β(π΄ β π΅)))) | ||
Theorem | fvvolioof 43940 | The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β (,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))(,)(2nd β(πΉβπ))))) | ||
Theorem | volioore 43941 | The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) = if(π΄ β€ π΅, (π΅ β π΄), 0)) | ||
Theorem | fvvolicof 43942 | The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β [,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))[,)(2nd β(πΉβπ))))) | ||
Theorem | voliooico 43943 | An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄(,)π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | ismbl4 43944* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl 24812, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β(vol*βπ₯) = ((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))))) | ||
Theorem | volioofmpt 43945* | ((vol β (,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β* Γ β*)) β β’ (π β ((vol β (,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicoff 43946 | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ):π΄βΆ(0[,]+β)) | ||
Theorem | voliooicof 43947 | The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β)) β β’ (π β ((vol β (,)) β πΉ) = ((vol β [,)) β πΉ)) | ||
Theorem | volicofmpt 43948* | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicc 43949 | The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | voliccico 43950 | A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄[,]π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | mbfdmssre 43951 | The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (πΉ β MblFn β dom πΉ β β) | ||
Theorem | stoweidlem1 43952 | Lemma for stoweid 44014. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 14058. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π΄ β β+) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ 1) & β’ (π β π· β€ π΄) β β’ (π β ((1 β (π΄βπ))β(πΎβπ)) β€ (1 / ((πΎ Β· π·)βπ))) | ||
Theorem | stoweidlem2 43953* | lemma for stoweid 44014: 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 43954* | Lemma for stoweid 44014: if π΄ is positive and all π terms of a finite product are larger than π΄, then the finite product is larger than π΄βπ. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππΉ & β’ β²ππ & β’ π = seq1( Β· , πΉ) & β’ (π β π β β) & β’ (π β πΉ:(1...π)βΆβ) & β’ ((π β§ π β (1...π)) β π΄ < (πΉβπ)) & β’ (π β π΄ β β+) β β’ (π β (π΄βπ) < (πβπ)) | ||
Theorem | stoweidlem4 43955* | Lemma for stoweid 44014: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ π΅ β β) β (π‘ β π β¦ π΅) β π΄) | ||
Theorem | stoweidlem5 43956* | 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.) |
β’ β²π‘π & β’ π· = if(πΆ β€ (1 / 2), πΆ, (1 / 2)) & β’ (π β π:πβΆβ) & β’ (π β π β π) & β’ (π β πΆ β β+) & β’ (π β βπ‘ β π πΆ β€ (πβπ‘)) β β’ (π β βπ(π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘))) | ||
Theorem | stoweidlem6 43957* | Lemma for stoweid 44014: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘ π = πΉ & β’ β²π‘ π = πΊ & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) Β· (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem7 43958* | This lemma is used to prove that qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that qn < Ξ΅ on π β π, and qn > 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.) |
β’ πΉ = (π β β0 β¦ ((1 / π΄)βπ)) & β’ πΊ = (π β β0 β¦ (π΅βπ)) & β’ (π β π΄ β β) & β’ (π β 1 < π΄) & β’ (π β π΅ β β+) & β’ (π β π΅ < 1) & β’ (π β πΈ β β+) β β’ (π β βπ β β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ)) | ||
Theorem | stoweidlem8 43959* | Lemma for stoweid 44014: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ β²π‘πΉ & β’ β²π‘πΊ β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) + (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem9 43960* | Lemma for stoweid 44014: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π = β ) & β’ (π β (π‘ β π β¦ 1) β π΄) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stoweidlem10 43961 | Lemma for stoweid 44014. 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.) |
β’ ((π΄ β β β§ π β β0 β§ π΄ β€ 1) β (1 β (π Β· π΄)) β€ ((1 β π΄)βπ)) | ||
Theorem | stoweidlem11 43962* | 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.) |
β’ (π β π β β) & β’ (π β π‘ β π) & β’ (π β π β (1...π)) & β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) & β’ ((π β§ π β (0...π)) β ((πβπ)βπ‘) β€ 1) & β’ ((π β§ π β (π...π)) β ((πβπ)βπ‘) < (πΈ / π)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) < ((π + (1 / 3)) Β· πΈ)) | ||
Theorem | stoweidlem12 43963* | Lemma for stoweid 44014. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π:πβΆβ) & β’ (π β π β β0) & β’ (π β πΎ β β0) β β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) | ||
Theorem | stoweidlem13 43964 | Lemma for stoweid 44014. 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.) |
β’ (π β πΈ β β+) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β ((π β (4 / 3)) Β· πΈ) < π) & β’ (π β π β€ ((π β (1 / 3)) Β· πΈ)) & β’ (π β ((π β (4 / 3)) Β· πΈ) < π) & β’ (π β π < ((π + (1 / 3)) Β· πΈ)) β β’ (π β (absβ(π β π)) < (2 Β· πΈ)) | ||
Theorem | stoweidlem14 43965* | 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.) |
β’ π΄ = {π β β β£ (1 / π·) < π} & β’ (π β π· β β+) & β’ (π β π· < 1) β β’ (π β βπ β β (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) | ||
Theorem | stoweidlem15 43966* | 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_(t0) = 0, and p > 0 on T - U. Here (πΊβπΌ) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (((π β§ πΌ β (1...π)) β§ π β π) β (((πΊβπΌ)βπ) β β β§ 0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) | ||
Theorem | stoweidlem16 43967* | Lemma for stoweid 44014. The subset π of functions in the algebra π΄, with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π» = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β β’ ((π β§ π β π β§ π β π) β π» β π) | ||
Theorem | stoweidlem17 43968* | 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.) |
β’ β²π‘π & β’ (π β π β β) & β’ (π β π:(0...π)βΆπ΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΈ β β) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (π β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) | ||
Theorem | stoweidlem18 43969* | 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.) |
β’ β²π‘π· & β’ β²π‘π & β’ πΉ = (π‘ β π β¦ 1) & β’ π = βͺ π½ & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β πΈ β β+) & β’ (π β π· = β ) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem19 43970* | 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.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΉ β π΄) & β’ (π β π β β0) β β’ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) | ||
Theorem | stoweidlem20 43971* | 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.) |
β’ β²π‘π & β’ πΉ = (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (π β πΉ β π΄) | ||
Theorem | stoweidlem21 43972* | 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.) |
β’ β²π‘πΊ & β’ β²π‘π» & β’ β²π‘π & β’ β²π‘π & β’ πΊ = (π‘ β π β¦ ((π»βπ‘) + π)) & β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β βπ β π΄ π:πβΆβ) & β’ (π β π» β π΄) & β’ (π β βπ‘ β π (absβ((π»βπ‘) β ((πΉβπ‘) β π))) < πΈ) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stoweidlem22 43973* | 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.) |
β’ β²π‘π & β’ β²π‘πΉ & β’ β²π‘πΊ & β’ π» = (π‘ β π β¦ ((πΉβπ‘) β (πΊβπ‘))) & β’ πΌ = (π‘ β π β¦ -1) & β’ πΏ = (π‘ β π β¦ ((πΌβπ‘) Β· (πΊβπ‘))) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) β (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem23 43974* | This lemma is used to prove the existence of a function pt 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 pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘πΊ & β’ π» = (π‘ β π β¦ ((πΊβπ‘) β (πΊβπ))) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΊ β π΄) & β’ (π β (πΊβπ) β (πΊβπ)) β β’ (π β (π» β π΄ β§ (π»βπ) β (π»βπ) β§ (π»βπ) = 0)) | ||
Theorem | stoweidlem24 43975* | This lemma proves that for π sufficiently large, qn( t ) > ( 1 - epsilon ), for all π‘ in π: see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). π is used to represent qn in the paper, π to represent π in the paper, πΎ to represent π, π· to represent Ξ΄, and πΈ to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π:πβΆβ) & β’ (π β π β β0) & β’ (π β πΎ β β0) & β’ (π β π· β β+) & β’ (π β πΈ β β+) & β’ (π β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) β β’ ((π β§ π‘ β π) β (1 β πΈ) < (πβπ‘)) | ||
Theorem | stoweidlem25 43976* | This lemma proves that for n sufficiently large, qn( t ) < Ξ΅, for all π‘ in π β π: see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). π is used to represent qn 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.) |
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π:πβΆβ) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) & β’ (π β πΈ β β+) & β’ (π β (1 / ((πΎ Β· π·)βπ)) < πΈ) β β’ ((π β§ π‘ β (π β π)) β (πβπ‘) < πΈ) | ||
Theorem | stoweidlem26 43977* | 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.) |
β’ β²π‘πΉ & β’ β²ππ & β’ β²π‘π & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ (π β π β β) & β’ (π β π β V) & β’ (π β πΏ β (1...π)) & β’ (π β π β ((π·βπΏ) β (π·β(πΏ β 1)))) & β’ (π β πΉ:πβΆβ) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) & β’ ((π β§ π β (0...π) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) & β’ ((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) β β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ)) | ||
Theorem | stoweidlem27 43978* | 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_(t0) = 0, and p > 0 on T - U. Here (πβπ) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ πΊ = (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) & β’ (π β π β V) & β’ (π β π β β) & β’ (π β π Fn ran πΊ) & β’ (π β ran πΊ β V) & β’ ((π β§ π β ran πΊ) β (πβπ) β π) & β’ (π β πΉ:(1...π)β1-1-ontoβran πΊ) & β’ (π β (π β π) β βͺ π) & β’ β²π‘π & β’ β²π€π & β’ β²βπ β β’ (π β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) | ||
Theorem | stoweidlem28 43979* | 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.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ (π β π β (π½ Cn πΎ)) & β’ (π β βπ‘ β (π β π)0 < (πβπ‘)) & β’ (π β π β π½) β β’ (π β βπ(π β β+ β§ π < 1 β§ βπ‘ β (π β π)π β€ (πβπ‘))) | ||
Theorem | stoweidlem29 43980* | 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.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β (inf(ran πΉ, β, < ) β ran πΉ β§ inf(ran πΉ, β, < ) β β β§ βπ‘ β π inf(ran πΉ, β, < ) β€ (πΉβπ‘))) | ||
Theorem | stoweidlem30 43981* | 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_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (πΊβπ) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ ((π β§ π β π) β (πβπ) = ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ))) | ||
Theorem | stoweidlem31 43982* | 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 β€ xi β€ 1, xi < Ξ΅ / m on V(ti), and xi > 1 - Ξ΅ / m on π΅. Here M is used to represent m in the paper, πΈ is used to represent Ξ΅ in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²βπ & β’ β²π‘π & β’ β²π€π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ πΊ = (π€ β π β¦ {β β π΄ β£ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < (πΈ / π) β§ βπ‘ β (π β π)(1 β (πΈ / π)) < (ββπ‘))}) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β π£:(1...π)β1-1-ontoβπ ) & β’ (π β πΈ β β+) & β’ (π β π΅ β (π β π)) & β’ (π β π β V) & β’ (π β π΄ β V) & β’ (π β ran πΊ β Fin) β β’ (π β βπ₯(π₯:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π₯βπ)βπ‘)))) | ||
Theorem | stoweidlem32 43983* | 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.) |
β’ β²π‘π & β’ π = (π‘ β π β¦ (π Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ πΉ = (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) & β’ π» = (π‘ β π β¦ π) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (π β π β π΄) | ||
Theorem | stoweidlem33 43984* | 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 43985* | 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.) |
β’ β²π‘πΉ & β’ β²ππ & β’ β²π‘π & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ π½ = (π‘ β π β¦ {π β (1...π) β£ π‘ β (π·βπ)}) & β’ (π β π β β) & β’ (π β π β V) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π‘ β π) β 0 β€ (πΉβπ‘)) & β’ ((π β§ π‘ β π) β (πΉβπ‘) < ((π β 1) Β· πΈ)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) & β’ ((π β§ π β (0...π) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) & β’ ((π β§ π β (0...π) β§ π‘ β π) β ((πβπ)βπ‘) β€ 1) & β’ ((π β§ π β (0...π) β§ π‘ β (π·βπ)) β ((πβπ)βπ‘) < (πΈ / π)) & β’ ((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) β β’ (π β βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘)))) | ||
Theorem | stoweidlem35 43986* | 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_(t0) = 0, and p > 0 on T - U. Here (πβπ) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π€π & β’ β²βπ & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ πΊ = (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) & β’ (π β π΄ β V) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β (π β π) β βͺ π) & β’ (π β (π β π) β β ) β β’ (π β βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) | ||
Theorem | stoweidlem36 43987* | This lemma is used to prove the existence of a function pt 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 pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Z is used for t0 , S is used for t e. T - U , h is used for pt . G is used for (ht)^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.) |
β’ β²βπ & β’ β²π‘π» & β’ β²π‘πΉ & β’ β²π‘πΊ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = βͺ π½ & β’ πΊ = (π‘ β π β¦ ((πΉβπ‘) Β· (πΉβπ‘))) & β’ π = sup(ran πΊ, β, < ) & β’ π» = (π‘ β π β¦ ((πΊβπ‘) / π)) & β’ (π β π½ β Comp) & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ β π΄) & β’ (π β (πΉβπ) β (πΉβπ)) & β’ (π β (πΉβπ) = 0) β β’ (π β ββ(β β π β§ 0 < (ββπ))) | ||
Theorem | stoweidlem37 43988* | 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_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (πΊβπ) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β π β π) β β’ (π β (πβπ) = 0) | ||
Theorem | stoweidlem38 43989* | 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_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (πΊβπ) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ ((π β§ π β π) β (0 β€ (πβπ) β§ (πβπ) β€ 1)) | ||
Theorem | stoweidlem39 43990* | 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 β€ xi β€ 1, xi < Ξ΅ / m on V(ti), and xi > 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 vi is used to represent V(ti). π is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²βπ & β’ β²π‘π & β’ β²π€π & β’ π = (π β π΅) & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ (π β π β (π« π β© Fin)) & β’ (π β π· β βͺ π) & β’ (π β π· β β ) & β’ (π β πΈ β β+) & β’ (π β π΅ β π) & β’ (π β π β V) & β’ (π β π΄ β V) β β’ (π β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran π£ β§ βπ₯(π₯:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π₯βπ)βπ‘))))) | ||
Theorem | stoweidlem40 43991* | This lemma proves that qn is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent qn 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.) |
β’ β²π‘π & β’ β²π‘π & β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))βπ)) & β’ πΉ = (π‘ β π β¦ (1 β ((πβπ‘)βπ))) & β’ πΊ = (π‘ β π β¦ 1) & β’ π» = (π‘ β π β¦ ((πβπ‘)βπ)) & β’ (π β π β π΄) & β’ (π β π:πβΆβ) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β β) & β’ (π β π β β) β β’ (π β π β π΄) | ||
Theorem | stoweidlem41 43992* | 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 - qn";. Here πΈ is used to represent Ξ΅ in the paper, and π¦ to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π = (π‘ β π β¦ (1 β (π¦βπ‘))) & β’ πΉ = (π‘ β π β¦ 1) & β’ π β π & β’ (π β π¦ β π΄) & β’ (π β π¦:πβΆβ) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π€ β β) β (π‘ β π β¦ π€) β π΄) & β’ (π β πΈ β β+) & β’ (π β βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)) & β’ (π β βπ‘ β π (1 β πΈ) < (π¦βπ‘)) & β’ (π β βπ‘ β (π β π)(π¦βπ‘) < πΈ) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem42 43993* | 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.) |
β’ β²ππ & β’ β²π‘π & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((πβπ)βπ‘)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ ((π β§ π β π) β π:πβΆβ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β V) & β’ (π β π΅ β π) β β’ (π β βπ‘ β π΅ (1 β πΈ) < (πβπ‘)) | ||
Theorem | stoweidlem43 43994* | This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function pt in the subalgebra, such that pt( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Hera Z is used for t0 , S is used for t e. T - U , h is used for pt. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²βπ & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) & β’ (π β π β (π β π)) β β’ (π β ββ(β β π β§ 0 < (ββπ))) | ||
Theorem | stoweidlem44 43995* | 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_(t0) = 0, and p > 0 on T - U. Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ (π β βπ‘ β (π β π)βπ β (1...π)0 < ((πΊβπ)βπ‘)) & β’ π = βͺ π½ & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β π) β β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) | ||
Theorem | stoweidlem45 43996* | This lemma proves that, given an appropriate πΎ (in another theorem we prove such a πΎ exists), there exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= qn <= 1 , qn < Ξ΅ on T \ U, and qn > 1 - Ξ΅ on π. We use y to represent the final qn 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.) |
β’ β²π‘π & β’ β²π‘π & β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π· < 1) & β’ (π β π β π΄) & β’ (π β π:πβΆβ) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΈ β β+) & β’ (π β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) & β’ (π β (1 / ((πΎ Β· π·)βπ)) < πΈ) β β’ (π β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) | ||
Theorem | stoweidlem46 43997* | 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.) |
β’ β²π‘π & β’ β²βπ & β’ β²ππ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) & β’ (π β π β V) β β’ (π β (π β π) β βͺ π) | ||
Theorem | stoweidlem47 43998* | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ β²π‘π & β’ π = βͺ π½ & β’ πΊ = (π Γ {-π}) & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Top) & β’ πΆ = (π½ Cn πΎ) & β’ (π β πΉ β πΆ) & β’ (π β π β β) β β’ (π β (π‘ β π β¦ ((πΉβπ‘) β π)) β πΆ) | ||
Theorem | stoweidlem48 43999* | 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.) |
β’ β²ππ & β’ β²π‘π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ (π β π:(1...π)βΆπ) & β’ (π β π· β βͺ ran π) & β’ (π β π· β π) & β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < πΈ) & β’ (π β π β V) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ (π β πΈ β β+) β β’ (π β βπ‘ β π· (πβπ‘) < πΈ) | ||
Theorem | stoweidlem49 44000* | There exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= qn <= 1 , qn < Ξ΅ on π β π, and qn > 1 - Ξ΅ on π. Here y is used to represent the final qn 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.) |
β’ β²π‘π & β’ β²π‘π & β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ (π β π· β β+) & β’ (π β π· < 1) & β’ (π β π β π΄) & β’ (π β π:πβΆβ) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΈ β β+) β β’ (π β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |