![]() |
Metamath
Proof Explorer Theorem List (p. 456 of 480) | < 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: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | meaiininclem 45501* | Measures are continuous from above: if πΈ is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Meas) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβ(π + 1)) β (πΈβπ)) & β’ (π β πΎ β (β€β₯βπ)) & β’ (π β (πβ(πΈβπΎ)) β β) & β’ π = (π β π β¦ (πβ(πΈβπ))) & β’ πΊ = (π β π β¦ ((πΈβπΎ) β (πΈβπ))) & β’ πΉ = βͺ π β π (πΊβπ) β β’ (π β π β (πββ© π β π (πΈβπ))) | ||
Theorem | meaiininc 45502* | Measures are continuous from above: if πΈ is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Meas) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβ(π + 1)) β (πΈβπ)) & β’ (π β πΎ β (β€β₯βπ)) & β’ (π β (πβ(πΈβπΎ)) β β) & β’ π = (π β π β¦ (πβ(πΈβπ))) β β’ (π β π β (πββ© π β π (πΈβπ))) | ||
Theorem | meaiininc2 45503* | Measures are continuous from above: if πΈ is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β Meas) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβ(π + 1)) β (πΈβπ)) & β’ (π β βπ β π (πβ(πΈβπ)) β β) & β’ π = (π β π β¦ (πβ(πΈβπ))) β β’ (π β π β (πββ© π β π (πΈβπ))) | ||
Proofs for most of the theorems in section 113 of [Fremlin1] | ||
Syntax | come 45504 | Extend class notation with the class of outer measures. |
class OutMeas | ||
Definition | df-ome 45505* | Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ OutMeas = {π₯ β£ ((((π₯:dom π₯βΆ(0[,]+β) β§ dom π₯ = π« βͺ dom π₯) β§ (π₯ββ ) = 0) β§ βπ¦ β π« βͺ dom π₯βπ§ β π« π¦(π₯βπ§) β€ (π₯βπ¦)) β§ βπ¦ β π« dom π₯(π¦ βΌ Ο β (π₯ββͺ π¦) β€ (Ξ£^β(π₯ βΎ π¦))))} | ||
Syntax | ccaragen 45506 | Extend class notation with a function that takes an outer measure and generates a sigma-algebra and a measure. |
class CaraGen | ||
Definition | df-caragen 45507* | Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ CaraGen = (π β OutMeas β¦ {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) | ||
Theorem | caragenval 45508* | The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β OutMeas β (CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) | ||
Theorem | isome 45509* | Express the predicate "π is an outer measure." Definition 113A of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β (π β OutMeas β ((((π:dom πβΆ(0[,]+β) β§ dom π = π« βͺ dom π) β§ (πββ ) = 0) β§ βπ¦ β π« βͺ dom πβπ§ β π« π¦(πβπ§) β€ (πβπ¦)) β§ βπ¦ β π« dom π(π¦ βΌ Ο β (πββͺ π¦) β€ (Ξ£^β(π βΎ π¦)))))) | ||
Theorem | caragenel 45510* | Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) β β’ (π β (πΈ β π β (πΈ β π« βͺ dom π β§ βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)))) | ||
Theorem | omef 45511 | An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π β β’ (π β π:π« πβΆ(0[,]+β)) | ||
Theorem | ome0 45512 | The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) β β’ (π β (πββ ) = 0) | ||
Theorem | omessle 45513 | The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) β β’ (π β (πβπ΄) β€ (πβπ΅)) | ||
Theorem | omedm 45514 | The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β OutMeas β dom π = π« βͺ dom π) | ||
Theorem | caragensplit 45515 | If πΈ is in the set generated by the Caratheodory's method, then it splits any set π΄ in two parts such that the sum of the outer measures of the two parts is equal to the outer measure of the whole set π΄. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ π = βͺ dom π & β’ (π β πΈ β π) & β’ (π β π΄ β π) β β’ (π β ((πβ(π΄ β© πΈ)) +π (πβ(π΄ β πΈ))) = (πβπ΄)) | ||
Theorem | caragenelss 45516 | An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β π΄ β π) & β’ π = βͺ dom π β β’ (π β π΄ β π) | ||
Theorem | carageneld 45517* | Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (CaraGenβπ) & β’ (π β πΈ β π« π) & β’ ((π β§ π β π« π) β ((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)) β β’ (π β πΈ β π) | ||
Theorem | omecl 45518 | The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β (0[,]+β)) | ||
Theorem | caragenss 45519 | The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the domain of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ π = (CaraGenβπ) β β’ (π β OutMeas β π β dom π) | ||
Theorem | omeunile 45520 | The outer measure of the union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π β π« π) & β’ (π β π βΌ Ο) β β’ (π β (πββͺ π) β€ (Ξ£^β(π βΎ π))) | ||
Theorem | caragen0 45521 | The empty set belongs to any Caratheodory's construction. First part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) β β’ (π β β β π) | ||
Theorem | omexrcl 45522 | The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β β*) | ||
Theorem | caragenunidm 45523 | The base set of an outer measure belongs to the sigma-algebra generated by the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (CaraGenβπ) β β’ (π β π β π) | ||
Theorem | caragensspw 45524 | The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the power set of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (CaraGenβπ) β β’ (π β π β π« π) | ||
Theorem | omessre 45525 | If the outer measure of a set is real, then the outer measure of any of its subset is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) & β’ (π β (πβπ΄) β β) & β’ (π β π΅ β π΄) β β’ (π β (πβπ΅) β β) | ||
Theorem | caragenuni 45526 | The base set of the sigma-algebra generated by the Caratheodory's construction is the whole base set of the original outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) β β’ (π β βͺ π = βͺ dom π) | ||
Theorem | caragenuncllem 45527 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ π = βͺ dom π & β’ (π β π΄ β π) β β’ (π β ((πβ(π΄ β© (πΈ βͺ πΉ))) +π (πβ(π΄ β (πΈ βͺ πΉ)))) = (πβπ΄)) | ||
Theorem | caragenuncl 45528 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (πΈ βͺ πΉ) β π) | ||
Theorem | caragendifcl 45529 | The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β πΈ β π) β β’ (π β (βͺ π β πΈ) β π) | ||
Theorem | caragenfiiuncl 45530* | The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) β β’ (π β βͺ π β π΄ π΅ β π) | ||
Theorem | omeunle 45531 | The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (πβ(π΄ βͺ π΅)) β€ ((πβπ΄) +π (πβπ΅))) | ||
Theorem | omeiunle 45532* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππΈ & β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ« π) β β’ (π β (πββͺ π β π (πΈβπ)) β€ (Ξ£^β(π β π β¦ (πβ(πΈβπ))))) | ||
Theorem | omelesplit 45533 | The outer measure of a set π΄ is less than or equal to the extended addition of the outer measures of the decomposition induced on π΄ by any πΈ. Step (a) in the proof of Caratheodory's Method, Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β€ ((πβ(π΄ β© πΈ)) +π (πβ(π΄ β πΈ)))) | ||
Theorem | omeiunltfirp 45534* | If the outer measure of a countable union is not +β, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ« π) & β’ (π β (πββͺ π β π (πΈβπ)) β β) & β’ (π β π β β+) β β’ (π β βπ§ β (π« π β© Fin)(πββͺ π β π (πΈβπ)) < (Ξ£π β π§ (πβ(πΈβπ)) + π)) | ||
Theorem | omeiunlempt 45535* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β πΈ β π) β β’ (π β (πββͺ π β π πΈ) β€ (Ξ£^β(π β π β¦ (πβπΈ)))) | ||
Theorem | carageniuncllem1 45536* | The outer measure of π΄ β© (πΊβπ) is the sum of the outer measures of π΄ β© (πΉβπ). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ π = βͺ dom π & β’ (π β π΄ β π) & β’ (π β (πβπ΄) β β) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ) & β’ πΊ = (π β π β¦ βͺ π β (π...π)(πΈβπ)) & β’ πΉ = (π β π β¦ ((πΈβπ) β βͺ π β (π..^π)(πΈβπ))) & β’ (π β πΎ β π) β β’ (π β Ξ£π β (π...πΎ)(πβ(π΄ β© (πΉβπ))) = (πβ(π΄ β© (πΊβπΎ)))) | ||
Theorem | carageniuncllem2 45537* | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ π = βͺ dom π & β’ (π β π΄ β π) & β’ (π β (πβπ΄) β β) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ) & β’ (π β π β β+) & β’ πΊ = (π β π β¦ βͺ π β (π...π)(πΈβπ)) & β’ πΉ = (π β π β¦ ((πΈβπ) β βͺ π β (π..^π)(πΈβπ))) β β’ (π β ((πβ(π΄ β© βͺ π β π (πΈβπ))) +π (πβ(π΄ β βͺ π β π (πΈβπ)))) β€ ((πβπ΄) + π)) | ||
Theorem | carageniuncl 45538* | The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ) β β’ (π β βͺ π β π (πΈβπ) β π) | ||
Theorem | caragenunicl 45539 | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ (π β π β π) & β’ (π β π βΌ Ο) β β’ (π β βͺ π β π) | ||
Theorem | caragensal 45540 | Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) β β’ (π β π β SAlg) | ||
Theorem | caratheodorylem1 45541* | Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ) & β’ (π β Disj π β π (πΈβπ)) & β’ πΊ = (π β π β¦ βͺ π β (π...π)(πΈβπ)) & β’ (π β π β (β€β₯βπ)) β β’ (π β (πβ(πΊβπ)) = (Ξ£^β(π β (π...π) β¦ (πβ(πΈβπ))))) | ||
Theorem | caratheodorylem2 45542* | Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (CaraGenβπ) & β’ (π β πΈ:ββΆπ) & β’ (π β Disj π β β (πΈβπ)) & β’ πΊ = (π β β β¦ βͺ π β (1...π)(πΈβπ)) β β’ (π β (πββͺ π β β (πΈβπ)) = (Ξ£^β(π β β β¦ (πβ(πΈβπ))))) | ||
Theorem | caratheodory 45543 | Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β OutMeas) & β’ π = (CaraGenβπ) β β’ (π β (π βΎ π) β Meas) | ||
Theorem | 0ome 45544* | The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β π) & β’ π = (π₯ β π« π β¦ 0) β β’ (π β π β OutMeas) | ||
Theorem | isomenndlem 45545* | π is sub-additive w.r.t. countable indexed union, implies that π is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π:π« πβΆ(0[,]+β)) & β’ (π β (πββ ) = 0) & β’ (π β π β π« π) & β’ ((π β§ π:ββΆπ« π) β (πββͺ π β β (πβπ)) β€ (Ξ£^β(π β β β¦ (πβ(πβπ))))) & β’ (π β π΅ β β) & β’ (π β πΉ:π΅β1-1-ontoβπ) & β’ π΄ = (π β β β¦ if(π β π΅, (πΉβπ), β )) β β’ (π β (πββͺ π) β€ (Ξ£^β(π βΎ π))) | ||
Theorem | isomennd 45546* | Sufficient condition to prove that π is an outer measure. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β π) & β’ (π β π:π« πβΆ(0[,]+β)) & β’ (π β (πββ ) = 0) & β’ ((π β§ π₯ β π β§ π¦ β π₯) β (πβπ¦) β€ (πβπ₯)) & β’ ((π β§ π:ββΆπ« π) β (πββͺ π β β (πβπ)) β€ (Ξ£^β(π β β β¦ (πβ(πβπ))))) β β’ (π β π β OutMeas) | ||
Theorem | caragenel2d 45547* | Membership in the Caratheodory's construction. Similar to carageneld 45517, but here "less then or equal to" is used, instead of equality. This is Remark 113D of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ π = (CaraGenβπ) & β’ (π β πΈ β π« π) & β’ ((π β§ π β π« π) β ((πβ(π β© πΈ)) +π (πβ(π β πΈ))) β€ (πβπ)) β β’ (π β πΈ β π) | ||
Theorem | omege0 45548 | If the outer measure of a set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) β β’ (π β 0 β€ (πβπ΄)) | ||
Theorem | omess0 45549 | If the outer measure of a set is 0, then the outer measure of its subsets is 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β π΄ β π) & β’ (π β (πβπ΄) = 0) & β’ (π β π΅ β π΄) β β’ (π β (πβπ΅) = 0) | ||
Theorem | caragencmpl 45550 | A measure built with the Caratheodory's construction is complete. See Definition 112Df of [Fremlin1] p. 19. This is Exercise 113Xa of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β OutMeas) & β’ π = βͺ dom π & β’ (π β πΈ β π) & β’ (π β (πβπΈ) = 0) & β’ π = (CaraGenβπ) β β’ (π β πΈ β π) | ||
Proofs for most of the theorems in section 115 of [Fremlin1] | ||
Syntax | covoln 45551 | Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers. |
class voln* | ||
Definition | df-ovoln 45552* | Define the outer measure for the space of multidimensional real numbers. The cardinality of π₯ is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ voln* = (π₯ β Fin β¦ (π¦ β π« (β βm π₯) β¦ if(π₯ = β , 0, inf({π§ β β* β£ βπ β (((β Γ β) βm π₯) βm β)(π¦ β βͺ π β β Xπ β π₯ (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π₯ (volβ(([,) β (πβπ))βπ)))))}, β*, < )))) | ||
Syntax | cvoln 45553 | Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers. |
class voln | ||
Definition | df-voln 45554 | Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of π₯ is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ voln = (π₯ β Fin β¦ ((voln*βπ₯) βΎ (CaraGenβ(voln*βπ₯)))) | ||
Theorem | vonval 45555 | Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) β β’ (π β (volnβπ) = ((voln*βπ) βΎ (CaraGenβ(voln*βπ)))) | ||
Theorem | ovnval 45556* | Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) β β’ (π β (voln*βπ) = (π¦ β π« (β βm π) β¦ if(π = β , 0, inf({π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π¦ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}, β*, < )))) | ||
Theorem | elhoi 45557* | Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β π) β β’ (π β (π β ((π΄[,)π΅) βm π) β (π:πβΆβ* β§ βπ₯ β π (πβπ₯) β (π΄[,)π΅)))) | ||
Theorem | icoresmbl 45558 | A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ran ([,) βΎ (β Γ β)) β dom vol | ||
Theorem | hoissre 45559* | The projection of a half-open interval onto a single dimension is a subset of β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β πΌ:πβΆ(β Γ β)) β β’ ((π β§ π β π) β (([,) β πΌ)βπ) β β) | ||
Theorem | ovnval2 45560* | Value of the Lebesgue outer measure of a subset π΄ of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β’ (π β ((voln*βπ)βπ΄) = if(π = β , 0, inf(π, β*, < ))) | ||
Theorem | volicorecl 45561 | The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) β β) | ||
Theorem | hoiprodcl 45562* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β πΌ:πβΆ(β Γ β)) β β’ (π β βπ β π (volβ(([,) β πΌ)βπ)) β (0[,)+β)) | ||
Theorem | hoicvr 45563* | πΌ is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ πΌ = (π β β β¦ (π₯ β π β¦ β¨-π, πβ©)) & β’ (π β π β Fin) β β’ (π β (β βm π) β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) | ||
Theorem | hoissrrn 45564* | A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β πΌ:πβΆ(β Γ β)) β β’ (π β Xπ β π (([,) β πΌ)βπ) β (β βm π)) | ||
Theorem | ovn0val 45565 | The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β (β βm β )) β β’ (π β ((voln*ββ )βπ΄) = 0) | ||
Theorem | ovnn0val 45566* | The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄ β (β βm π)) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β’ (π β ((voln*βπ)βπ΄) = inf(π, β*, < )) | ||
Theorem | ovnval2b 45567* | Value of the Lebesgue outer measure of a subset π΄ of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ πΏ = (π β π« (β βm π) β¦ {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) β β’ (π β ((voln*βπ)βπ΄) = if(π = β , 0, inf((πΏβπ΄), β*, < ))) | ||
Theorem | volicorescl 45568 | The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π΄ β ran ([,) βΎ (β Γ β)) β (volβπ΄) β β) | ||
Theorem | ovnprodcl 45569* | The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β πΉ:ββΆ((β Γ β) βm π)) & β’ (π β πΌ β β) β β’ (π β βπ β π (volβ(([,) β (πΉβπΌ))βπ)) β (0[,)+β)) | ||
Theorem | hoiprodcl2 45570* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π β Fin) & β’ πΏ = (π β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β π)βπ))) & β’ (π β πΌ:πβΆ(β Γ β)) β β’ (π β (πΏβπΌ) β (0[,)+β)) | ||
Theorem | hoicvrrex 45571* | Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β (β βm π)) β β’ (π β βπ β (((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ +β = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) | ||
Theorem | ovnsupge0 45572* | The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β’ (π β π β (0[,]+β)) | ||
Theorem | ovnlecvr 45573* | Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with π the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ πΏ = (π β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β π)βπ))) & β’ (π β πΌ:ββΆ((β Γ β) βm π)) & β’ (π β π΄ β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) β β’ (π β ((voln*βπ)βπ΄) β€ (Ξ£^β(π β β β¦ (πΏβ(πΌβπ))))) | ||
Theorem | ovnpnfelsup 45574* | +β is an element of the set used in the definition of the Lebesgue outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β’ (π β +β β π) | ||
Theorem | ovnsslelem 45575* | The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (β βm π)) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΅ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β’ (π β ((voln*βπ)βπ΄) β€ ((voln*βπ)βπ΅)) | ||
Theorem | ovnssle 45576 | The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (β βm π)) β β’ (π β ((voln*βπ)βπ΄) β€ ((voln*βπ)βπ΅)) | ||
Theorem | ovnlerp 45577* | The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄ β (β βm π)) & β’ (π β πΈ β β+) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β’ (π β βπ§ β π π§ β€ (((voln*βπ)βπ΄) +π πΈ)) | ||
Theorem | ovnf 45578 | The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) β β’ (π β (voln*βπ):π« (β βm π)βΆ(0[,]+β)) | ||
Theorem | ovncvrrp 45579* | The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄ β (β βm π)) & β’ (π β πΈ β β+) & β’ πΆ = (π β π« (β βm π) β¦ {π β (((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) & β’ πΏ = (β β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) & β’ π· = (π β π« (β βm π) β¦ (π β β+ β¦ {π β (πΆβπ) β£ (Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) β β’ (π β βπ π β ((π·βπ΄)βπΈ)) | ||
Theorem | ovn0lem 45580* | For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))} & β’ (π β inf(π, β*, < ) β (0[,]+β)) & β’ πΌ = (π β β β¦ (π β π β¦ β¨1, 0β©)) β β’ (π β inf(π, β*, < ) = 0) | ||
Theorem | ovn0 45581 | For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) β β’ (π β ((voln*βπ)ββ ) = 0) | ||
Theorem | ovncl 45582 | The Lebesgue outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) β β’ (π β ((voln*βπ)βπ΄) β (0[,]+β)) | ||
Theorem | ovn02 45583 | For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (voln*ββ ) = (π₯ β π« {β } β¦ 0) | ||
Theorem | ovnxrcl 45584 | The Lebesgue outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) β β’ (π β ((voln*βπ)βπ΄) β β*) | ||
Theorem | ovnsubaddlem1 45585* | The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:ββΆπ« (β βm π)) & β’ (π β πΈ β β+) & β’ π = (π β π« (β βm π) β¦ {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) & β’ πΆ = (π β π« (β βm π) β¦ {β β (((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (ββπ))βπ)}) & β’ πΏ = (π β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β π)βπ))) & β’ π· = (π β π« (β βm π) β¦ (π β β+ β¦ {π β (πΆβπ) β£ (Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) & β’ ((π β§ π β β) β (πΌβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) & β’ (π β πΉ:ββ1-1-ontoβ(β Γ β)) & β’ πΊ = (π β β β¦ ((πΌβ(1st β(πΉβπ)))β(2nd β(πΉβπ)))) β β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€ ((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) | ||
Theorem | ovnsubaddlem2 45586* | (voln*βπ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:ββΆπ« (β βm π)) & β’ (π β πΈ β β+) & β’ π = (π β π« (β βm π) β¦ {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) & β’ πΆ = (π β π« (β βm π) β¦ {π β (((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) & β’ πΏ = (β β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) & β’ π· = (π β π« (β βm π) β¦ (π β β+ β¦ {π β (πΆβπ) β£ (Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) β β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€ ((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) | ||
Theorem | ovnsubadd 45587* | (voln*βπ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) & β’ (π β π΄:ββΆπ« (β βm π)) β β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€ (Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ))))) | ||
Theorem | ovnome 45588 | (voln*βπ) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set π. Proposition 115D (a) of [Fremlin1] p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) β β’ (π β (voln*βπ) β OutMeas) | ||
Theorem | vonmea 45589 | (volnβπ) is a measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set π. Comments in Definition 115E of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π β Fin) β β’ (π β (volnβπ) β Meas) | ||
Theorem | volicon0 45590 | The measure of a nonempty left-closed, right-open interval. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) β β’ (π β (volβ(π΄[,)π΅)) = (π΅ β π΄)) | ||
Theorem | hsphoif 45591* | π» is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ (π β π΄ β β) & β’ (π β π β π) & β’ (π β π΅:πβΆβ) β β’ (π β ((π»βπ΄)βπ΅):πβΆβ) | ||
Theorem | hoidmvval 45592* | The dimensional volume of a multidimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β π β Fin) β β’ (π β (π΄(πΏβπ)π΅) = if(π = β , 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ))))) | ||
Theorem | hoissrrn2 45593* | A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β*) β β’ (π β Xπ β π (π΄[,)π΅) β (β βm π)) | ||
Theorem | hsphoival 45594* | π» is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ (π β π΄ β β) & β’ (π β π β π) & β’ (π β π΅:πβΆβ) & β’ (π β πΎ β π) β β’ (π β (((π»βπ΄)βπ΅)βπΎ) = if(πΎ β π, (π΅βπΎ), if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄))) | ||
Theorem | hoiprodcl3 45595* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β βπ β π (volβ(π΄[,)π΅)) β (0[,)+β)) | ||
Theorem | volicore 45596 | The Lebesgue measure of a left-closed right-open interval is a real number. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) β β) | ||
Theorem | hoidmvcl 45597* | The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) β β’ (π β (π΄(πΏβπ)π΅) β (0[,)+β)) | ||
Theorem | hoidmv0val 45598* | The dimensional volume of a 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π΄:β βΆβ) & β’ (π β π΅:β βΆβ) β β’ (π β (π΄(πΏββ )π΅) = 0) | ||
Theorem | hoidmvn0val 45599* | The dimensional volume of a non-0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) β β’ (π β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) | ||
Theorem | hsphoidmvle2 45600* | The dimensional volume of a half-open interval intersected with a two half-spaces. Used in the last inequality of step (c) of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ β€ π·) & β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) β β’ (π β (π΄(πΏβπ)((π»βπΆ)βπ΅)) β€ (π΄(πΏβπ)((π»βπ·)βπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |