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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ovolsca 24801* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β+) & β’ (π β π΅ = {π₯ β β β£ (πΆ Β· π₯) β π΄}) & β’ (π β (vol*βπ΄) β β) β β’ (π β (vol*βπ΅) = ((vol*βπ΄) / πΆ)) | ||
Theorem | ovolicc1 24802* | 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 24803* | Lemma for ovolicc2 24808. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) β β’ ((π β§ π β π) β (π β π β (π β β β§ (1st β(πΉβ(πΊβπ))) < π β§ π < (2nd β(πΉβ(πΊβπ)))))) | ||
Theorem | ovolicc2lem2 24804* | Lemma for ovolicc2 24808. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } & β’ (π β π»:πβΆπ) & β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) & β’ (π β π΄ β πΆ) & β’ (π β πΆ β π) & β’ πΎ = seq1((π» β 1st ), (β Γ {πΆ})) & β’ π = {π β β β£ π΅ β (πΎβπ)} β β’ ((π β§ (π β β β§ Β¬ π β π)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅) | ||
Theorem | ovolicc2lem3 24805* | Lemma for ovolicc2 24808. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } & β’ (π β π»:πβΆπ) & β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) & β’ (π β π΄ β πΆ) & β’ (π β πΆ β π) & β’ πΎ = seq1((π» β 1st ), (β Γ {πΆ})) & β’ π = {π β β β£ π΅ β (πΎβπ)} β β’ ((π β§ (π β {π β β β£ βπ β π π β€ π} β§ π β {π β β β£ βπ β π π β€ π})) β (π = π β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ)))))) | ||
Theorem | ovolicc2lem4 24806* | Lemma for ovolicc2 24808. (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 24807* | Lemma for ovolicc2 24808. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) & β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β } β β’ (π β (π΅ β π΄) β€ sup(ran π, β*, < )) | ||
Theorem | ovolicc2 24808* | 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 24809 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (vol*β(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | ovolicopnf 24810 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (π΄ β β β (vol*β(π΄[,)+β)) = +β) | ||
Theorem | ovolre 24811 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ (vol*ββ) = +β | ||
Theorem | ismbl 24812* | 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 24813* | From ovolun 24785, 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 24814 | A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.) |
β’ vol = (vol* βΎ dom vol) | ||
Theorem | volf 24815 | The domain and codomain of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.) |
β’ vol:dom volβΆ(0[,]+β) | ||
Theorem | mblvol 24816 | 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 24817 | A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.) |
β’ (π΄ β dom vol β π΄ β β) | ||
Theorem | mblsplit 24818 | The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β β§ (vol*βπ΅) β β) β (vol*βπ΅) = ((vol*β(π΅ β© π΄)) + (vol*β(π΅ β π΄)))) | ||
Theorem | volss 24819 | 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 24820 | The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ (π΄ β dom vol β (β β π΄) β dom vol) | ||
Theorem | nulmbl 24821 | A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β β β§ (vol*βπ΄) = 0) β π΄ β dom vol) | ||
Theorem | nulmbl2 24822* | 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 24823 | A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol) β (π΄ βͺ π΅) β dom vol) | ||
Theorem | shftmbl 24824* | A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β) β {π₯ β β β£ (π₯ β π΅) β π΄} β dom vol) | ||
Theorem | 0mbl 24825 | The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ β β dom vol | ||
Theorem | rembl 24826 | The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ β β dom vol | ||
Theorem | unidmvol 24827 | The union of the Lebesgue measurable sets is β. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ βͺ dom vol = β | ||
Theorem | inmbl 24828 | An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol) β (π΄ β© π΅) β dom vol) | ||
Theorem | difmbl 24829 | A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β dom vol β§ π΅ β dom vol) β (π΄ β π΅) β dom vol) | ||
Theorem | finiunmbl 24830* | A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol) β βͺ π β π΄ π΅ β dom vol) | ||
Theorem | volun 24831 | 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 24832 | Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (((π΄ β dom vol β§ π΅ β dom vol) β§ ((volβπ΄) β β β§ (volβπ΅) β β)) β ((volβπ΄) + (volβπ΅)) = ((volβ(π΄ β© π΅)) + (volβ(π΄ βͺ π΅)))) | ||
Theorem | volfiniun 24833* | 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 24834* | Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π = π β π΄ = π΅) β β’ βͺ π β β π΄ = βͺ π β β (π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | iundisj2 24835* | A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ (π = π β π΄ = π΅) β β’ Disj π β β (π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | voliunlem1 24836* | Lemma for voliun 24840. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π β πΉ:ββΆdom vol) & β’ (π β Disj π β β (πΉβπ)) & β’ π» = (π β β β¦ (vol*β(πΈ β© (πΉβπ)))) & β’ (π β πΈ β β) & β’ (π β (vol*βπΈ) β β) β β’ ((π β§ π β β) β ((seq1( + , π»)βπ) + (vol*β(πΈ β βͺ ran πΉ))) β€ (vol*βπΈ)) | ||
Theorem | voliunlem2 24837* | Lemma for voliun 24840. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π β πΉ:ββΆdom vol) & β’ (π β Disj π β β (πΉβπ)) & β’ π» = (π β β β¦ (vol*β(π₯ β© (πΉβπ)))) β β’ (π β βͺ ran πΉ β dom vol) | ||
Theorem | voliunlem3 24838* | Lemma for voliun 24840. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ (π β πΉ:ββΆdom vol) & β’ (π β Disj π β β (πΉβπ)) & β’ π» = (π β β β¦ (vol*β(π₯ β© (πΉβπ)))) & β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβ(πΉβπ))) & β’ (π β βπ β β (volβ(πΉβπ)) β β) β β’ (π β (volββͺ ran πΉ) = sup(ran π, β*, < )) | ||
Theorem | iunmbl 24839 | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ (βπ β β π΄ β dom vol β βͺ π β β π΄ β dom vol) | ||
Theorem | voliun 24840 | 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 24841* | Lemma for volsup 24842. (Contributed by Mario Carneiro, 4-Jul-2014.) |
β’ ((βπ β β (πΉβπ) β (πΉβ(π + 1)) β§ (π΄ β β β§ π΅ β (β€β₯βπ΄))) β (πΉβπ΄) β (πΉβπ΅)) | ||
Theorem | volsup 24842* | 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 24843* | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ βΌ β β§ βπ β π΄ π΅ β dom vol) β βͺ π β π΄ π΅ β dom vol) | ||
Theorem | ioombl1lem1 24844* | Lemma for ioombl1 24848. (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 24845* | Lemma for ioombl1 24848. (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 24846* | Lemma for ioombl1 24848. (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 24847* | Lemma for ioombl1 24848. (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 24848 | 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 24849 | A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ (π΄ β β β (π΄[,)+β) β dom vol) | ||
Theorem | icombl 24850 | A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β*) β (π΄[,)π΅) β dom vol) | ||
Theorem | ioombl 24851 | An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ (π΄(,)π΅) β dom vol | ||
Theorem | iccmbl 24852 | A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β dom vol) | ||
Theorem | iccvolcl 24853 | A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,]π΅)) β β) | ||
Theorem | ovolioo 24854 | The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (vol*β(π΄(,)π΅)) = (π΅ β π΄)) | ||
Theorem | volioo 24855 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,)π΅)) = (π΅ β π΄)) | ||
Theorem | ioovolcl 24856 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) β β) | ||
Theorem | ovolfs2 24857 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΊ = ((abs β β ) β πΉ) β β’ (πΉ:ββΆ( β€ β© (β Γ β)) β πΊ = ((vol* β (,)) β πΉ)) | ||
Theorem | ioorcl2 24858 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (((π΄(,)π΅) β β β§ (vol*β(π΄(,)π΅)) β β) β (π΄ β β β§ π΅ β β)) | ||
Theorem | ioorf 24859 | 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 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 (,) β (πΉβπ΄) = if(π΄ = β , β¨0, 0β©, β¨inf(π΄, β*, < ), sup(π΄, β*, < )β©)) | ||
Theorem | ioorinv2 24861* | 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 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(π₯, β*, < )β©)) β β’ (π΄ β ran (,) β ((,)β(πΉβπ΄)) = π΄) | ||
Theorem | ioorcl 24863* | 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 24864 | 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 24865* | 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 24840.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β (vol*ββͺ ran ((,) β πΉ)) = sup(ran π, β*, < )) | ||
Theorem | uniiccvol 24866* | 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 24840.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β (vol*ββͺ ran ([,] β πΉ)) = sup(ran π, β*, < )) | ||
Theorem | uniioombllem1 24867* | Lemma for uniioombl 24875. (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (π β sup(ran π, β*, < ) β β) | ||
Theorem | uniioombllem2a 24868* | Lemma for uniioombl 24875. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (((π β§ π½ β β) β§ π§ β β) β (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ran (,)) | ||
Theorem | uniioombllem2 24869* | Lemma for uniioombl 24875. (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 24870* | Lemma for uniioombl 24875. (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 24871* | Lemma for uniioombl 24875. (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 24872* | Lemma for uniioombl 24875. (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 24873* | Lemma for uniioombl 24875. (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 24874* | Lemma for uniioombl 24875. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) | ||
Theorem | uniioombl 24875* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24839.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ((,) β πΉ) β dom vol) | ||
Theorem | uniiccmbl 24876* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24839.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ([,] β πΉ) β dom vol) | ||
Theorem | dyadf 24877* | 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 24878* | Value of the dyadic rational function πΉ. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (π΄πΉπ΅) = β¨(π΄ / (2βπ΅)), ((π΄ + 1) / (2βπ΅))β©) | ||
Theorem | dyadovol 24879* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (vol*β([,]β(π΄πΉπ΅))) = (1 / (2βπ΅))) | ||
Theorem | dyadss 24880* | 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 24881* | Lemma for dyaddisj 24882. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β0 β§ π· β β0)) β§ πΆ β€ π·) β (([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·)) β¨ ([,]β(π΅πΉπ·)) β ([,]β(π΄πΉπΆ)) β¨ (((,)β(π΄πΉπΆ)) β© ((,)β(π΅πΉπ·))) = β )) | ||
Theorem | dyaddisj 24882* | 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 24883* | Lemma for dyadmax 24884. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β0) & β’ (π β π· β β0) & β’ (π β Β¬ π· < πΆ) & β’ (π β ([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·))) β β’ (π β (π΄ = π΅ β§ πΆ = π·)) | ||
Theorem | dyadmax 24884* | 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 24885* | Lemma for dyadmbl 24886. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) = βͺ ([,] β πΊ)) | ||
Theorem | dyadmbl 24886* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) β dom vol) | ||
Theorem | opnmbllem 24887* | Lemma for opnmbl 24888. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | opnmbl 24888 | All open sets are measurable. This proof, via dyadmbl 24886 and uniioombl 24875, 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 24889 | All open sets are measurable. This alternative proof of opnmbl 24888 is significantly shorter, at the expense of invoking countable choice ax-cc 10305. (This was also the original proof before the current opnmbl 24888 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | subopnmbl 24890 | 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 24891* | 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 24892* | 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 24893* | 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 24894* | Lemma for vitali 24899. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} β β’ βΌ Er (0[,]1) | ||
Theorem | vitalilem2 24895* | Lemma for vitali 24899. (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 24896* | Lemma for vitali 24899. (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 24897* | Lemma for vitali 24899. (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 24898* | Lemma for vitali 24899. (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 24899 | 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 β π« β) | ||
Syntax | cmbf 24900 | Extend class notation with the class of measurable functions. |
class MblFn |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |