Home | Metamath
Proof Explorer Theorem List (p. 249 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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ovolscalem2 24801* | Lemma for ovolshft 24798. (Contributed by Mario Carneiro, 22-Mar-2014.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β+) & β’ (π β π΅ = {π₯ β β β£ (πΆ Β· π₯) β π΄}) & β’ (π β (vol*βπ΄) β β) β β’ (π β (vol*βπ΅) β€ ((vol*βπ΄) / πΆ)) | ||
Theorem | ovolsca 24802* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β+) & β’ (π β π΅ = {π₯ β β β£ (πΆ Β· π₯) β π΄}) & β’ (π β (vol*βπ΄) β β) β β’ (π β (vol*βπ΅) = ((vol*βπ΄) / πΆ)) | ||
Theorem | ovolicc1 24803* | The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ πΊ = (π β β β¦ if(π = 1, β¨π΄, π΅β©, β¨0, 0β©)) β β’ (π β (vol*β(π΄[,]π΅)) β€ (π΅ β π΄)) | ||
Theorem | ovolicc2lem1 24804* | Lemma for ovolicc2 24809. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) β β’ ((π β§ π β π) β (π β π β (π β β β§ (1st β(πΉβ(πΊβπ))) < π β§ π < (2nd β(πΉβ(πΊβπ)))))) | ||
Theorem | ovolicc2lem2 24805* | Lemma for ovolicc2 24809. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } & β’ (π β π»:πβΆπ) & β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) & β’ (π β π΄ β πΆ) & β’ (π β πΆ β π) & β’ πΎ = seq1((π» β 1st ), (β Γ {πΆ})) & β’ π = {π β β β£ π΅ β (πΎβπ)} β β’ ((π β§ (π β β β§ Β¬ π β π)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅) | ||
Theorem | ovolicc2lem3 24806* | Lemma for ovolicc2 24809. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } & β’ (π β π»:πβΆπ) & β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) & β’ (π β π΄ β πΆ) & β’ (π β πΆ β π) & β’ πΎ = seq1((π» β 1st ), (β Γ {πΆ})) & β’ π = {π β β β£ π΅ β (πΎβπ)} β β’ ((π β§ (π β {π β β β£ βπ β π π β€ π} β§ π β {π β β β£ βπ β π π β€ π})) β (π = π β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ)))))) | ||
Theorem | ovolicc2lem4 24807* | Lemma for ovolicc2 24809. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by AV, 17-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } & β’ (π β π»:πβΆπ) & β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) & β’ (π β π΄ β πΆ) & β’ (π β πΆ β π) & β’ πΎ = seq1((π» β 1st ), (β Γ {πΆ})) & β’ π = {π β β β£ π΅ β (πΎβπ)} & β’ π = inf(π, β, < ) β β’ (π β (π΅ β π΄) β€ sup(ran π, β*, < )) | ||
Theorem | ovolicc2lem5 24808* | Lemma for ovolicc2 24809. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } β β’ (π β (π΅ β π΄) β€ sup(ran π, β*, < )) | ||
Theorem | ovolicc2 24809* | The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)((π΄[,]π΅) β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} β β’ (π β (π΅ β π΄) β€ (vol*β(π΄[,]π΅))) | ||
Theorem | ovolicc 24810 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (vol*β(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | ovolicopnf 24811 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π΄ β β β (vol*β(π΄[,)+β)) = +β) | ||
Theorem | ovolre 24812 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (vol*ββ) = +β | ||
Theorem | ismbl 24813* | The predicate "π΄ is Lebesgue-measurable". A set is measurable if it splits every other set π₯ in a "nice" way, that is, if the measure of the pieces π₯ β© π΄ and π₯ β π΄ sum up to the measure of π₯ (assuming that the measure of π₯ is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β((vol*βπ₯) β β β (vol*βπ₯) = ((vol*β(π₯ β© π΄)) + (vol*β(π₯ β π΄)))))) | ||
Theorem | ismbl2 24814* | From ovolun 24786, it suffices to show that the measure of π₯ is at least the sum of the measures of π₯ β© π΄ and π₯ β π΄. (Contributed by Mario Carneiro, 15-Jun-2014.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β((vol*βπ₯) β β β ((vol*β(π₯ β© π΄)) + (vol*β(π₯ β π΄))) β€ (vol*βπ₯)))) | ||
Theorem | volres 24815 | A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.) |
β’ vol = (vol* βΎ dom vol) | ||
Theorem | volf 24816 | The domain and codomain of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.) |
β’ vol:dom volβΆ(0[,]+β) | ||
Theorem | mblvol 24817 | The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014.) |
β’ (π΄ β dom vol β (volβπ΄) = (vol*βπ΄)) | ||
Theorem | mblss 24818 | A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.) |
β’ (π΄ β dom vol β π΄ β β) | ||
Theorem | mblsplit 24819 | The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β β§ (vol*βπ΅) β β) β (vol*βπ΅) = ((vol*β(π΅ β© π΄)) + (vol*β(π΅ β π΄)))) | ||
Theorem | volss 24820 | The Lebesgue measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 17-Oct-2017.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol β§ π΄ β π΅) β (volβπ΄) β€ (volβπ΅)) | ||
Theorem | cmmbl 24821 | The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ (π΄ β dom vol β (β β π΄) β dom vol) | ||
Theorem | nulmbl 24822 | A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β β β§ (vol*βπ΄) = 0) β π΄ β dom vol) | ||
Theorem | nulmbl2 24823* | A set of outer measure zero is measurable. The term "outer measure zero" here is slightly different from "nullset/negligible set"; a nullset has vol*(π΄) = 0 while "outer measure zero" means that for any π₯ there is a π¦ containing π΄ with volume less than π₯. Assuming AC, these notions are equivalent (because the intersection of all such π¦ is a nullset) but in ZF this is a strictly weaker notion. Proposition 563Gb of [Fremlin5] p. 193. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (βπ₯ β β+ βπ¦ β dom vol(π΄ β π¦ β§ (vol*βπ¦) β€ π₯) β π΄ β dom vol) | ||
Theorem | unmbl 24824 | A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol) β (π΄ βͺ π΅) β dom vol) | ||
Theorem | shftmbl 24825* | A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β) β {π₯ β β β£ (π₯ β π΅) β π΄} β dom vol) | ||
Theorem | 0mbl 24826 | The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ β β dom vol | ||
Theorem | rembl 24827 | The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ β β dom vol | ||
Theorem | unidmvol 24828 | The union of the Lebesgue measurable sets is β. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ βͺ dom vol = β | ||
Theorem | inmbl 24829 | An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol) β (π΄ β© π΅) β dom vol) | ||
Theorem | difmbl 24830 | A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol) β (π΄ β π΅) β dom vol) | ||
Theorem | finiunmbl 24831* | A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β βͺ π β π΄ π΅ β dom vol) | ||
Theorem | volun 24832 | The Lebesgue measure function is finitely additive. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ (((π΄ β dom vol β§ π΅ β dom vol β§ (π΄ β© π΅) = β ) β§ ((volβπ΄) β β β§ (volβπ΅) β β)) β (volβ(π΄ βͺ π΅)) = ((volβπ΄) + (volβπ΅))) | ||
Theorem | volinun 24833 | Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (((π΄ β dom vol β§ π΅ β dom vol) β§ ((volβπ΄) β β β§ (volβπ΅) β β)) β ((volβπ΄) + (volβπ΅)) = ((volβ(π΄ β© π΅)) + (volβ(π΄ βͺ π΅)))) | ||
Theorem | volfiniun 24834* | The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ ((π΄ β Fin β§ βπ β π΄ (π΅ β dom vol β§ (volβπ΅) β β) β§ Disj π β π΄ π΅) β (volββͺ π β π΄ π΅) = Ξ£π β π΄ (volβπ΅)) | ||
Theorem | iundisj 24835* | Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π = π β π΄ = π΅) β β’ βͺ π β β π΄ = βͺ π β β (π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | iundisj2 24836* | A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ (π = π β π΄ = π΅) β β’ Disj π β β (π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | voliunlem1 24837* | Lemma for voliun 24841. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π β πΉ:ββΆdom vol) & β’ (π β Disj π β β (πΉβπ)) & β’ π» = (π β β β¦ (vol*β(πΈ β© (πΉβπ)))) & β’ (π β πΈ β β) & β’ (π β (vol*βπΈ) β β) β β’ ((π β§ π β β) β ((seq1( + , π»)βπ) + (vol*β(πΈ β βͺ ran πΉ))) β€ (vol*βπΈ)) | ||
Theorem | voliunlem2 24838* | Lemma for voliun 24841. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π β πΉ:ββΆdom vol) & β’ (π β Disj π β β (πΉβπ)) & β’ π» = (π β β β¦ (vol*β(π₯ β© (πΉβπ)))) β β’ (π β βͺ ran πΉ β dom vol) | ||
Theorem | voliunlem3 24839* | Lemma for voliun 24841. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π β πΉ:ββΆdom vol) & β’ (π β Disj π β β (πΉβπ)) & β’ π» = (π β β β¦ (vol*β(π₯ β© (πΉβπ)))) & β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβ(πΉβπ))) & β’ (π β βπ β β (volβ(πΉβπ)) β β) β β’ (π β (volββͺ ran πΉ) = sup(ran π, β*, < )) | ||
Theorem | iunmbl 24840 | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ (βπ β β π΄ β dom vol β βͺ π β β π΄ β dom vol) | ||
Theorem | voliun 24841 | The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβπ΄)) β β’ ((βπ β β (π΄ β dom vol β§ (volβπ΄) β β) β§ Disj π β β π΄) β (volββͺ π β β π΄) = sup(ran π, β*, < )) | ||
Theorem | volsuplem 24842* | Lemma for volsup 24843. (Contributed by Mario Carneiro, 4-Jul-2014.) |
β’ ((βπ β β (πΉβπ) β (πΉβ(π + 1)) β§ (π΄ β β β§ π΅ β (β€β₯βπ΄))) β (πΉβπ΄) β (πΉβπ΅)) | ||
Theorem | volsup 24843* | The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ ((πΉ:ββΆdom vol β§ βπ β β (πΉβπ) β (πΉβ(π + 1))) β (volββͺ ran πΉ) = sup((vol β ran πΉ), β*, < )) | ||
Theorem | iunmbl2 24844* | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ βΌ β β§ βπ β π΄ π΅ β dom vol) β βͺ π β π΄ π΅ β dom vol) | ||
Theorem | ioombl1lem1 24845* | Lemma for ioombl1 24849. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ π΅ = (π΄(,)+β) & β’ (π β π΄ β β) & β’ (π β πΈ β β) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ π = seq1( + , ((abs β β ) β π»)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΉ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ π = (1st β(πΉβπ)) & β’ π = (2nd β(πΉβπ)) & β’ πΊ = (π β β β¦ β¨if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π), πβ©) & β’ π» = (π β β β¦ β¨π, if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π)β©) β β’ (π β (πΊ:ββΆ( β€ β© (β Γ β)) β§ π»:ββΆ( β€ β© (β Γ β)))) | ||
Theorem | ioombl1lem2 24846* | Lemma for ioombl1 24849. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ π΅ = (π΄(,)+β) & β’ (π β π΄ β β) & β’ (π β πΈ β β) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ π = seq1( + , ((abs β β ) β π»)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΉ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ π = (1st β(πΉβπ)) & β’ π = (2nd β(πΉβπ)) & β’ πΊ = (π β β β¦ β¨if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π), πβ©) & β’ π» = (π β β β¦ β¨π, if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π)β©) β β’ (π β sup(ran π, β*, < ) β β) | ||
Theorem | ioombl1lem3 24847* | Lemma for ioombl1 24849. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ π΅ = (π΄(,)+β) & β’ (π β π΄ β β) & β’ (π β πΈ β β) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ π = seq1( + , ((abs β β ) β π»)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΉ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ π = (1st β(πΉβπ)) & β’ π = (2nd β(πΉβπ)) & β’ πΊ = (π β β β¦ β¨if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π), πβ©) & β’ π» = (π β β β¦ β¨π, if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π)β©) β β’ ((π β§ π β β) β ((((abs β β ) β πΊ)βπ) + (((abs β β ) β π»)βπ)) = (((abs β β ) β πΉ)βπ)) | ||
Theorem | ioombl1lem4 24848* | Lemma for ioombl1 24849. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ π΅ = (π΄(,)+β) & β’ (π β π΄ β β) & β’ (π β πΈ β β) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ π = seq1( + , ((abs β β ) β π»)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΉ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ π = (1st β(πΉβπ)) & β’ π = (2nd β(πΉβπ)) & β’ πΊ = (π β β β¦ β¨if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π), πβ©) & β’ π» = (π β β β¦ β¨π, if(if(π β€ π΄, π΄, π) β€ π, if(π β€ π΄, π΄, π), π)β©) β β’ (π β ((vol*β(πΈ β© π΅)) + (vol*β(πΈ β π΅))) β€ ((vol*βπΈ) + πΆ)) | ||
Theorem | ioombl1 24849 | An open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.) |
β’ (π΄ β β* β (π΄(,)+β) β dom vol) | ||
Theorem | icombl1 24850 | A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ (π΄ β β β (π΄[,)+β) β dom vol) | ||
Theorem | icombl 24851 | A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β*) β (π΄[,)π΅) β dom vol) | ||
Theorem | ioombl 24852 | An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ (π΄(,)π΅) β dom vol | ||
Theorem | iccmbl 24853 | A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β dom vol) | ||
Theorem | iccvolcl 24854 | A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,]π΅)) β β) | ||
Theorem | ovolioo 24855 | The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (vol*β(π΄(,)π΅)) = (π΅ β π΄)) | ||
Theorem | volioo 24856 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,)π΅)) = (π΅ β π΄)) | ||
Theorem | ioovolcl 24857 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) β β) | ||
Theorem | ovolfs2 24858 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΊ = ((abs β β ) β πΉ) β β’ (πΉ:ββΆ( β€ β© (β Γ β)) β πΊ = ((vol* β (,)) β πΉ)) | ||
Theorem | ioorcl2 24859 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (((π΄(,)π΅) β β β§ (vol*β(π΄(,)π΅)) β β) β (π΄ β β β§ π΅ β β)) | ||
Theorem | ioorf 24860 | Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β , β¨0, 0β©, β¨inf(π₯, β*, < ), sup(π₯, β*, < )β©)) β β’ πΉ:ran (,)βΆ( β€ β© (β* Γ β*)) | ||
Theorem | ioorval 24861* | Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β , β¨0, 0β©, β¨inf(π₯, β*, < ), sup(π₯, β*, < )β©)) β β’ (π΄ β ran (,) β (πΉβπ΄) = if(π΄ = β , β¨0, 0β©, β¨inf(π΄, β*, < ), sup(π΄, β*, < )β©)) | ||
Theorem | ioorinv2 24862* | The function πΉ is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β , β¨0, 0β©, β¨inf(π₯, β*, < ), sup(π₯, β*, < )β©)) β β’ ((π΄(,)π΅) β β β (πΉβ(π΄(,)π΅)) = β¨π΄, π΅β©) | ||
Theorem | ioorinv 24863* | The function πΉ is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β , β¨0, 0β©, β¨inf(π₯, β*, < ), sup(π₯, β*, < )β©)) β β’ (π΄ β ran (,) β ((,)β(πΉβπ΄)) = π΄) | ||
Theorem | ioorcl 24864* | The function πΉ does not always return real numbers, but it does on intervals of finite volume. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β , β¨0, 0β©, β¨inf(π₯, β*, < ), sup(π₯, β*, < )β©)) β β’ ((π΄ β ran (,) β§ (vol*βπ΄) β β) β (πΉβπ΄) β ( β€ β© (β Γ β))) | ||
Theorem | uniiccdif 24865 | A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) β β’ (π β (βͺ ran ((,) β πΉ) β βͺ ran ([,] β πΉ) β§ (vol*β(βͺ ran ([,] β πΉ) β βͺ ran ((,) β πΉ))) = 0)) | ||
Theorem | uniioovol 24866* | A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 24841.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β (vol*ββͺ ran ((,) β πΉ)) = sup(ran π, β*, < )) | ||
Theorem | uniiccvol 24867* | An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 24841.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β (vol*ββͺ ran ([,] β πΉ)) = sup(ran π, β*, < )) | ||
Theorem | uniioombllem1 24868* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (π β sup(ran π, β*, < ) β β) | ||
Theorem | uniioombllem2a 24869* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (((π β§ π½ β β) β§ π§ β β) β (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ran (,)) | ||
Theorem | uniioombllem2 24870* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by AV, 13-Sep-2020.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ π» = (π§ β β β¦ (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) & β’ πΎ = (π₯ β ran (,) β¦ if(π₯ = β , β¨0, 0β©, β¨inf(π₯, β*, < ), sup(π₯, β*, < )β©)) β β’ ((π β§ π½ β β) β seq1( + , (vol* β π»)) β (vol*β(((,)β(πΊβπ½)) β© π΄))) | ||
Theorem | uniioombllem3a 24871* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) β β’ (π β (πΎ = βͺ π β (1...π)((,)β(πΊβπ)) β§ (vol*βπΎ) β β)) | ||
Theorem | uniioombllem3 24872* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) < (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ))) | ||
Theorem | uniioombllem4 24873* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) & β’ (π β π β β) & β’ (π β βπ β (1...π)(absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) & β’ πΏ = βͺ (((,) β πΉ) β (1...π)) β β’ (π β (vol*β(πΎ β© π΄)) β€ ((vol*β(πΎ β© πΏ)) + πΆ)) | ||
Theorem | uniioombllem5 24874* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) & β’ (π β π β β) & β’ (π β βπ β (1...π)(absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) & β’ πΏ = βͺ (((,) β πΉ) β (1...π)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) | ||
Theorem | uniioombllem6 24875* | Lemma for uniioombl 24876. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) | ||
Theorem | uniioombl 24876* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24840.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ((,) β πΉ) β dom vol) | ||
Theorem | uniiccmbl 24877* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24840.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ([,] β πΉ) β dom vol) | ||
Theorem | dyadf 24878* | The function πΉ returns the endpoints of a dyadic rational covering of the real line. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ πΉ:(β€ Γ β0)βΆ( β€ β© (β Γ β)) | ||
Theorem | dyadval 24879* | Value of the dyadic rational function πΉ. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (π΄πΉπ΅) = β¨(π΄ / (2βπ΅)), ((π΄ + 1) / (2βπ΅))β©) | ||
Theorem | dyadovol 24880* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (vol*β([,]β(π΄πΉπ΅))) = (1 / (2βπ΅))) | ||
Theorem | dyadss 24881* | Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) (Proof shortened by Mario Carneiro, 26-Apr-2016.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β0 β§ π· β β0)) β (([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·)) β π· β€ πΆ)) | ||
Theorem | dyaddisjlem 24882* | Lemma for dyaddisj 24883. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β0 β§ π· β β0)) β§ πΆ β€ π·) β (([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·)) β¨ ([,]β(π΅πΉπ·)) β ([,]β(π΄πΉπΆ)) β¨ (((,)β(π΄πΉπΆ)) β© ((,)β(π΅πΉπ·))) = β )) | ||
Theorem | dyaddisj 24883* | Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β ran πΉ β§ π΅ β ran πΉ) β (([,]βπ΄) β ([,]βπ΅) β¨ ([,]βπ΅) β ([,]βπ΄) β¨ (((,)βπ΄) β© ((,)βπ΅)) = β )) | ||
Theorem | dyadmaxlem 24884* | Lemma for dyadmax 24885. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β0) & β’ (π β π· β β0) & β’ (π β Β¬ π· < πΆ) & β’ (π β ([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·))) β β’ (π β (π΄ = π΅ β§ πΆ = π·)) | ||
Theorem | dyadmax 24885* | Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β ran πΉ β§ π΄ β β ) β βπ§ β π΄ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)) | ||
Theorem | dyadmbllem 24886* | Lemma for dyadmbl 24887. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) = βͺ ([,] β πΊ)) | ||
Theorem | dyadmbl 24887* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) β dom vol) | ||
Theorem | opnmbllem 24888* | Lemma for opnmbl 24889. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | opnmbl 24889 | All open sets are measurable. This proof, via dyadmbl 24887 and uniioombl 24876, shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | opnmblALT 24890 | All open sets are measurable. This alternative proof of opnmbl 24889 is significantly shorter, at the expense of invoking countable choice ax-cc 10305. (This was also the original proof before the current opnmbl 24889 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | subopnmbl 24891 | Sets which are open in a measurable subspace are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ π½ = ((topGenβran (,)) βΎt π΄) β β’ ((π΄ β dom vol β§ π΅ β π½) β π΅ β dom vol) | ||
Theorem | volsup2 24892* | The volume of π΄ is the supremum of the sequence vol*β(π΄ β© (-π[,]π)) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β β§ π΅ < (volβπ΄)) β βπ β β π΅ < (volβ(π΄ β© (-π[,]π)))) | ||
Theorem | volcn 24893* | The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ πΉ = (π₯ β β β¦ (volβ(π΄ β© (π΅[,]π₯)))) β β’ ((π΄ β dom vol β§ π΅ β β) β πΉ β (ββcnββ)) | ||
Theorem | volivth 24894* | The Intermediate Value Theorem for the Lebesgue volume function. For any positive π΅ β€ (volβπ΄), there is a measurable subset of π΄ whose volume is π΅. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΄ β dom vol β§ π΅ β (0[,](volβπ΄))) β βπ₯ β dom vol(π₯ β π΄ β§ (volβπ₯) = π΅)) | ||
Theorem | vitalilem1 24895* | Lemma for vitali 24900. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} β β’ βΌ Er (0[,]1) | ||
Theorem | vitalilem2 24896* | Lemma for vitali 24900. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ (π β (ran πΉ β (0[,]1) β§ (0[,]1) β βͺ π β β (πβπ) β§ βͺ π β β (πβπ) β (-1[,]2))) | ||
Theorem | vitalilem3 24897* | Lemma for vitali 24900. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ (π β Disj π β β (πβπ)) | ||
Theorem | vitalilem4 24898* | Lemma for vitali 24900. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ ((π β§ π β β) β (vol*β(πβπ)) = 0) | ||
Theorem | vitalilem5 24899* | Lemma for vitali 24900. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ Β¬ π | ||
Theorem | vitali 24900 | If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ( < We β β dom vol β π« β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |