![]() |
Metamath
Proof Explorer Theorem List (p. 457 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hoidmvval0 45601* | The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β βπ β π (π΅βπ) β€ (π΄βπ)) β β’ (π β (π΄(πΏβπ)π΅) = 0) | ||
Theorem | hoiprodp1 45602* | The dimensional volume of a half-open interval with dimension π + 1. Used in the first equality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β Β¬ π β π) & β’ π = (π βͺ {π}) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΊ = βπ β π (volβ((π΄βπ)[,)(π΅βπ))) β β’ (π β (π΄(πΏβπ)π΅) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) | ||
Theorem | sge0hsphoire 45603* | If the generalized sum of dimensional volumes of n-dimensional half-open intervals is finite, then the sum stays finite if every half-open interval is intersected with a half-space. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) & β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ (π β π β β) β β’ (π β (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) | ||
Theorem | hoidmvval0b 45604* | The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) β β’ (π β (π΄(πΏβπ)π΄) = 0) | ||
Theorem | hoidmv1lelem1 45605* | The supremum of π belongs to π. This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΆ:ββΆβ) & β’ (π β π·:ββΆβ) & β’ (π β (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ))))) β β) & β’ π = {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€ (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))} & β’ π = sup(π, β, < ) β β’ (π β (π β π β§ π΄ β π β§ βπ₯ β β βπ¦ β π π¦ β€ π₯)) | ||
Theorem | hoidmv1lelem2 45606* | This is the contradiction proven in step (c) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ:ββΆβ) & β’ (π β π·:ββΆβ) & β’ (π β (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ))))) β β) & β’ π = {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€ (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))} & β’ (π β π β π) & β’ (π β π΄ β€ π) & β’ (π β π < π΅) & β’ (π β πΎ β β) & β’ (π β π β ((πΆβπΎ)[,)(π·βπΎ))) & β’ π = if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β β’ (π β βπ’ β π π < π’) | ||
Theorem | hoidmv1lelem3 45607* | The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the nonempty, finite generalized sum, sub case in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΆ:ββΆβ) & β’ (π β π·:ββΆβ) & β’ (π β (π΄[,)π΅) β βͺ π β β ((πΆβπ)[,)(π·βπ))) & β’ (π β (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ))))) β β) & β’ π = {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€ (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))} & β’ π = sup(π, β, < ) β β’ (π β (π΅ β π΄) β€ (Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ)))))) | ||
Theorem | hoidmv1le 45608* | The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β π) & β’ π = {π} & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β β’ (π β (π΄(πΏβπ)π΅) β€ (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) | ||
Theorem | hoidmvlelem1 45609* | The supremum of π belongs to π. Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) & β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) & β’ (π β πΈ β β+) & β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β· (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} & β’ π = sup(π, β, < ) & β’ (π β (π΄βπ) < (π΅βπ)) β β’ (π β π β π) | ||
Theorem | hoidmvlelem2 45610* | This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β πΆ:ββΆ(β βm π)) & β’ πΉ = (π¦ β π β¦ 0) & β’ π½ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) & β’ (π β π·:ββΆ(β βm π)) & β’ πΎ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) & β’ (π β (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) & β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) & β’ (π β πΈ β β+) & β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β· (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} & β’ (π β π β π) & β’ (π β π < (π΅βπ)) & β’ π = (π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))) & β’ (π β π β β) & β’ (π β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) & β’ π = ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) & β’ π = ({(π΅βπ)} βͺ π) & β’ π = inf(π, β, < ) β β’ (π β βπ’ β π π < π’) | ||
Theorem | hoidmvlelem3 45611* | This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) & β’ πΉ = (π¦ β π β¦ 0) & β’ (π β πΆ:ββΆ(β βm π)) & β’ π½ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) & β’ (π β π·:ββΆ(β βm π)) & β’ πΎ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) & β’ (π β (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) & β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) & β’ (π β πΈ β β+) & β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β· (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} & β’ (π β π β π) & β’ (π β π < (π΅βπ)) & β’ π = (π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))) & β’ (π β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm β)ββ β ((β βm π) βm β)(Xπ β π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€ (Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) & β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) & β’ π = (π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β¦ (π β π β¦ if(π β π, (π₯βπ), π))) β β’ (π β βπ’ β π π < π’) | ||
Theorem | hoidmvlelem4 45612* | The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29, case nonempty interval and dimension of the space greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β π β β ) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) & β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) & β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) & β’ (π β πΈ β β+) & β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β· (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} & β’ π = sup(π, β, < ) & β’ (π β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm β)ββ β ((β βm π) βm β)(Xπ β π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€ (Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) & β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β β’ (π β (π΄(πΏβπ)π΅) β€ ((1 + πΈ) Β· (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))))) | ||
Theorem | hoidmvlelem5 45613* | The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β π β (π β π)) & β’ π = (π βͺ {π}) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm β)ββ β ((β βm π) βm β)(Xπ β π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€ (Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) & β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) & β’ (π β π β β ) β β’ (π β (π΄(πΏβπ)π΅) β€ (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) | ||
Theorem | hoidmvle 45614* | The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β β’ (π β (π΄(πΏβπ)π΅) β€ (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) | ||
Theorem | ovnhoilem1 45615* | The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} & β’ π» = (π β β β¦ (π β π β¦ if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©))) β β’ (π β ((voln*βπ)βπΌ) β€ βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) | ||
Theorem | ovnhoilem2 45616* | The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} & β’ πΉ = (π β (((β Γ β) βm π) βm β) β¦ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) & β’ π = (π β (((β Γ β) βm π) βm β) β¦ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))) β β’ (π β (π΄(πΏβπ)π΅) β€ ((voln*βπ)βπΌ)) | ||
Theorem | ovnhoi 45617* | The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) β β’ (π β ((voln*βπ)βπΌ) = (π΄(πΏβπ)π΅)) | ||
Theorem | dmovn 45618 | The domain of the Lebesgue outer measure is the power set of the n-dimensional Real numbers. Step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) β β’ (π β dom (voln*βπ) = π« (β βm π)) | ||
Theorem | hoicoto2 45619* | The half-open interval expressed using a composition of a function into (β Γ β) and using two distinct real-valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β πΌ:πβΆ(β Γ β)) & β’ π΄ = (π β π β¦ (1st β(πΌβπ))) & β’ π΅ = (π β π β¦ (2nd β(πΌβπ))) β β’ (π β Xπ β π (([,) β πΌ)βπ) = Xπ β π ((π΄βπ)[,)(π΅βπ))) | ||
Theorem | dmvon 45620 | Lebesgue measurable n-dimensional subsets of Reals. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) β β’ (π β dom (volnβπ) = (CaraGenβ(voln*βπ))) | ||
Theorem | hoi2toco 45621* | The half-open interval expressed using a composition of a function into (β Γ β) and using two distinct real-valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²ππ & β’ πΌ = (π β π β¦ β¨(π΄βπ), (π΅βπ)β©) β β’ (π β Xπ β π (([,) β πΌ)βπ) = Xπ β π ((π΄βπ)[,)(π΅βπ))) | ||
Theorem | hoidifhspval 45622* | π· is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π₯ β€ (πβπ), (πβπ), π₯), (πβπ))))) & β’ (π β π β β) β β’ (π β (π·βπ) = (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π β€ (πβπ), (πβπ), π), (πβπ))))) | ||
Theorem | hspval 45623* | The value of the half-space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β π₯ if(π = π, (-β(,)π¦), β))) & β’ (π β π β Fin) & β’ (π β πΌ β π) & β’ (π β π β β) β β’ (π β (πΌ(π»βπ)π) = Xπ β π if(π = πΌ, (-β(,)π), β)) | ||
Theorem | ovnlecvr2 45624* | 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. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β π΄ β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) β β’ (π β ((voln*βπ)βπ΄) β€ (Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) | ||
Theorem | ovncvr2 45625* | π΅ and π are the left and right side of a cover of π΄. This cover is made of n-dimensional half-open intervals and approximates the n-dimensional Lebesgue outer volume of π΄. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ (π β πΈ β β+) & β’ πΆ = (π β π« (β βm π) β¦ {π β (((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) & β’ πΏ = (β β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) & β’ π· = (π β π« (β βm π) β¦ (π β β+ β¦ {π β (πΆβπ) β£ (Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) & β’ (π β πΌ β ((π·βπ΄)βπΈ)) & β’ π΅ = (π β β β¦ (π β π β¦ (1st β((πΌβπ)βπ)))) & β’ π = (π β β β¦ (π β π β¦ (2nd β((πΌβπ)βπ)))) β β’ (π β (((π΅:ββΆ(β βm π) β§ π:ββΆ(β βm π)) β§ π΄ β βͺ π β β Xπ β π (((π΅βπ)βπ)[,)((πβπ)βπ))) β§ (Ξ£^β(π β β β¦ βπ β π (volβ(((π΅βπ)βπ)[,)((πβπ)βπ))))) β€ (((voln*βπ)βπ΄) +π πΈ))) | ||
Theorem | dmovnsal 45626 | The domain of the Lebesgue measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) β β’ (π β π β SAlg) | ||
Theorem | unidmovn 45627 | Base set of the n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) β β’ (π β βͺ dom (voln*βπ) = (β βm π)) | ||
Theorem | rrnmbl 45628 | The set of n-dimensional Real numbers is Lebesgue measurable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) β β’ (π β (β βm π) β dom (volnβπ)) | ||
Theorem | hoidifhspval2 45629* | π· is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π₯ β€ (πβπ), (πβπ), π₯), (πβπ))))) & β’ (π β π β β) & β’ (π β π β π) & β’ (π β π΄:πβΆβ) β β’ (π β ((π·βπ)βπ΄) = (π β π β¦ if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ)))) | ||
Theorem | hspdifhsp 45630* | A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β π₯ if(π = π, (-β(,)π¦), β))) β β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) = β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) | ||
Theorem | unidmvon 45631 | Base set of the n-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) β β’ (π β βͺ π = (β βm π)) | ||
Theorem | hoidifhspf 45632* | π· is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π₯ β€ (πβπ), (πβπ), π₯), (πβπ))))) & β’ (π β π β β) & β’ (π β π β π) & β’ (π β π΄:πβΆβ) β β’ (π β ((π·βπ)βπ΄):πβΆβ) | ||
Theorem | hoidifhspval3 45633* | π· is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π₯ β€ (πβπ), (πβπ), π₯), (πβπ))))) & β’ (π β π β β) & β’ (π β π β π) & β’ (π β π΄:πβΆβ) & β’ (π β π½ β π) β β’ (π β (((π·βπ)βπ΄)βπ½) = if(π½ = πΎ, if(π β€ (π΄βπ½), (π΄βπ½), π), (π΄βπ½))) | ||
Theorem | hoidifhspdmvle 45634* | The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β πΎ β π) & β’ π· = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β = πΎ, if(π₯ β€ (πββ), (πββ), π₯), (πββ))))) & β’ (π β π β β) β β’ (π β (((π·βπ)βπ΄)(πΏβπ)π΅) β€ (π΄(πΏβπ)π΅)) | ||
Theorem | voncmpl 45635 | The Lebesgue measure is complete. See Definition 112Df of [Fremlin1] p. 19. This is an observation written after Definition 115E of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β πΈ β dom (volnβπ)) & β’ (π β ((volnβπ)βπΈ) = 0) & β’ (π β πΉ β πΈ) β β’ (π β πΉ β π) | ||
Theorem | hoiqssbllem1 45636* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π β (β βm π)) & β’ (π β πΆ:πβΆβ) & β’ (π β π·:πβΆβ) & β’ (π β πΈ β β+) & β’ ((π β§ π β π) β (πΆβπ) β (((πβπ) β (πΈ / (2 Β· (ββ(β―βπ)))))(,)(πβπ))) & β’ ((π β§ π β π) β (π·βπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β· (ββ(β―βπ))))))) β β’ (π β π β Xπ β π ((πΆβπ)[,)(π·βπ))) | ||
Theorem | hoiqssbllem2 45637* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π β (β βm π)) & β’ (π β πΆ:πβΆβ) & β’ (π β π·:πβΆβ) & β’ (π β πΈ β β+) & β’ ((π β§ π β π) β (πΆβπ) β (((πβπ) β (πΈ / (2 Β· (ββ(β―βπ)))))(,)(πβπ))) & β’ ((π β§ π β π) β (π·βπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β· (ββ(β―βπ))))))) β β’ (π β Xπ β π ((πΆβπ)[,)(π·βπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) | ||
Theorem | hoiqssbllem3 45638* | A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π β (β βm π)) & β’ (π β πΈ β β+) β β’ (π β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) | ||
Theorem | hoiqssbl 45639* | A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β π β (β βm π)) & β’ (π β πΈ β β+) β β’ (π β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) | ||
Theorem | hspmbllem1 45640* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (a) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ (π β π β β) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ π = (π¦ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) & β’ π = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β = πΎ, if(π₯ β€ (πββ), (πββ), π₯), (πββ))))) β β’ (π β (π΄(πΏβπ)π΅) = ((π΄(πΏβπ)((πβπ)βπ΅)) +π (((πβπ)βπ΄)(πΏβπ)π΅))) | ||
Theorem | hspmbllem2 45641* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β π₯ if(π = π, (-β(,)π¦), β))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ (π β π β β) & β’ (π β πΈ β β+) & β’ (π β πΆ:ββΆ(β βm π)) & β’ (π β π·:ββΆ(β βm π)) & β’ (π β π΄ β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) & β’ (π β (Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))))) β€ (((voln*βπ)βπ΄) + πΈ)) & β’ (π β ((voln*βπ)βπ΄) β β) & β’ (π β ((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) β β) & β’ (π β ((voln*βπ)β(π΄ β (πΎ(π»βπ)π))) β β) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) & β’ π = (π¦ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) & β’ π = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β = πΎ, if(π₯ β€ (πββ), (πββ), π₯), (πββ))))) β β’ (π β (((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) + ((voln*βπ)β(π΄ β (πΎ(π»βπ)π)))) β€ (((voln*βπ)βπ΄) + πΈ)) | ||
Theorem | hspmbllem3 45642* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β π₯ if(π = π, (-β(,)π¦), β))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ (π β π β β) & β’ (π β ((voln*βπ)βπ΄) β β) & β’ (π β π΄ β (β βm π)) & β’ πΆ = (π β π« (β βm π) β¦ {π β (((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) & β’ πΏ = (β β ((β Γ β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) & β’ π· = (π β π« (β βm π) β¦ (π β β+ β¦ {π β (πΆβπ) β£ (Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) & β’ π΅ = (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) & β’ π = (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) β β’ (π β (((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) +π ((voln*βπ)β(π΄ β (πΎ(π»βπ)π)))) β€ ((voln*βπ)βπ΄)) | ||
Theorem | hspmbl 45643* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β π₯ if(π = π, (-β(,)π¦), β))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ (π β π β β) β β’ (π β (πΎ(π»βπ)π) β dom (volnβπ)) | ||
Theorem | hoimbllem 45644* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ π = dom (volnβπ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β π₯ if(π = π, (-β(,)π¦), β))) β β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β π) | ||
Theorem | hoimbl 45645* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) β β’ (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β π) | ||
Theorem | opnvonmbllem1 45646* | The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²ππ & β’ (π β π β π) & β’ (π β πΆ:πβΆβ) & β’ (π β π·:πβΆβ) & β’ (π β Xπ β π ((πΆβπ)[,)(π·βπ)) β π΅) & β’ (π β π΅ β πΊ) & β’ (π β π β Xπ β π ((πΆβπ)[,)(π·βπ))) & β’ πΎ = {β β ((β Γ β) βm π) β£ Xπ β π (([,) β β)βπ) β πΊ} & β’ π» = (π β π β¦ β¨(πΆβπ), (π·βπ)β©) β β’ (π β ββ β πΎ π β Xπ β π (([,) β β)βπ)) | ||
Theorem | opnvonmbllem2 45647* | An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β πΊ β (TopOpenβ(β^βπ))) & β’ πΎ = {β β ((β Γ β) βm π) β£ Xπ β π (([,) β β)βπ) β πΊ} β β’ (π β πΊ β π) | ||
Theorem | opnvonmbl 45648 | An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β πΊ β (TopOpenβ(β^βπ))) β β’ (π β πΊ β π) | ||
Theorem | opnssborel 45649 | Open sets of a generalized real Euclidean space are Borel sets (notice that this theorem is even more general, because π is not required to be a set). (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π΄ = (TopOpenβ(β^βπ)) & β’ π΅ = (SalGenβπ΄) β β’ π΄ β π΅ | ||
Theorem | borelmbl 45650 | All Borel subsets of the n-dimensional Real numbers are Lebesgue measurable. This is Proposition 115G (b) of [Fremlin1] p. 32. See also Definition 111G (d) of [Fremlin1] p. 13. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ π΅ = (SalGenβ(TopOpenβ(β^βπ))) β β’ (π β π΅ β π) | ||
Theorem | volicorege0 45651 | The Lebesgue measure of a left-closed right-open interval with real bounds, is a nonnegative real number. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) β (0[,)+β)) | ||
Theorem | isvonmbl 45652* | The predicate "π΄ is measurable w.r.t. the n-dimensional Lebesgue measure". 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 π₯. Definition 114E of [Fremlin1] p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) β β’ (π β (πΈ β dom (volnβπ) β (πΈ β (β βm π) β§ βπ β π« (β βm π)(((voln*βπ)β(π β© πΈ)) +π ((voln*βπ)β(π β πΈ))) = ((voln*βπ)βπ)))) | ||
Theorem | mblvon 45653 | The n-dimensional Lebesgue measure of a measurable set is the same as its n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β dom (volnβπ)) β β’ (π β ((volnβπ)βπ΄) = ((voln*βπ)βπ΄)) | ||
Theorem | vonmblss 45654 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) β β’ (π β dom (volnβπ) β π« (β βm π)) | ||
Theorem | volico2 45655 | The measure of left-closed right-open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) = if(π΄ β€ π΅, (π΅ β π΄), 0)) | ||
Theorem | vonmblss2 45656 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) & β’ (π β π β dom (volnβπ)) β β’ (π β π β (β βm π)) | ||
Theorem | ovolval2lem 45657* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Ξ£^. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) β β’ (π β ran seq1( + , ((abs β β ) β πΉ)) = ran (π β β β¦ Ξ£π β (1...π)(volβ(([,) β πΉ)βπ)))) | ||
Theorem | ovolval2 45658* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Ξ£^. See ovolval 25222 for an alternative expression. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = (Ξ£^β((abs β β ) β π)))} β β’ (π β (vol*βπ΄) = inf(π, β*, < )) | ||
Theorem | ovnsubadd2lem 45659* | (voln*βπ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ (π β π΅ β (β βm π)) & β’ πΆ = (π β β β¦ if(π = 1, π΄, if(π = 2, π΅, β ))) β β’ (π β ((voln*βπ)β(π΄ βͺ π΅)) β€ (((voln*βπ)βπ΄) +π ((voln*βπ)βπ΅))) | ||
Theorem | ovnsubadd2 45660 | (voln*βπ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ (π β π΅ β (β βm π)) β β’ (π β ((voln*βπ)β(π΄ βͺ π΅)) β€ (((voln*βπ)βπ΄) +π ((voln*βπ)βπ΅))) | ||
Theorem | ovolval3 45661* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Ξ£^ and vol β (,). See ovolval 25222 and ovolval2 45658 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = (Ξ£^β((vol β (,)) β π)))} β β’ (π β (vol*βπ΄) = inf(π, β*, < )) | ||
Theorem | ovnsplit 45662 | The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) β β’ (π β ((voln*βπ)βπ΄) β€ (((voln*βπ)β(π΄ β© π΅)) +π ((voln*βπ)β(π΄ β π΅)))) | ||
Theorem | ovolval4lem1 45663* | |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) π) = (((,) β πΉ) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:ββΆ(β* Γ β*)) & β’ πΊ = (π β β β¦ β¨(1st β(πΉβπ)), if((1st β(πΉβπ)) β€ (2nd β(πΉβπ)), (2nd β(πΉβπ)), (1st β(πΉβπ)))β©) & β’ π΄ = {π β β β£ (1st β(πΉβπ)) β€ (2nd β(πΉβπ))} β β’ (π β (βͺ ran ((,) β πΉ) = βͺ ran ((,) β πΊ) β§ (vol β ((,) β πΉ)) = (vol β ((,) β πΊ)))) | ||
Theorem | ovolval4lem2 45664* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 45661, but here π is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ π = {π¦ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = (Ξ£^β((vol β (,)) β π)))} & β’ πΊ = (π β β β¦ β¨(1st β(πβπ)), if((1st β(πβπ)) β€ (2nd β(πβπ)), (2nd β(πβπ)), (1st β(πβπ)))β©) β β’ (π β (vol*βπ΄) = inf(π, β*, < )) | ||
Theorem | ovolval4 45665* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 45661, but here π may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ π = {π¦ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = (Ξ£^β((vol β (,)) β π)))} β β’ (π β (vol*βπ΄) = inf(π, β*, < )) | ||
Theorem | ovolval5lem1 45666* | β’ (π β (Ξ£^β(π β β β¦ (volβ((π΄ β (π / (2βπ) ))(,)π΅)))) β€ ((Ξ£^β(π β β β¦ (volβ(π΄[,)π΅) ))) +π π)). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π β§ π β β) β π΄ β β) & β’ ((π β§ π β β) β π΅ β β) & β’ (π β π β β+) & β’ πΆ = {π β β β£ π΄ < π΅} β β’ (π β (Ξ£^β(π β β β¦ (volβ((π΄ β (π / (2βπ)))(,)π΅)))) β€ ((Ξ£^β(π β β β¦ (volβ(π΄[,)π΅)))) +π π)) | ||
Theorem | ovolval5lem2 45667* | β’ ((π β§ π β β) β β¨((1st β(πΉβπ)) β (π / (2βπ))), (2nd β(πΉβπ))β© β (β Γ β)). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ π = {π§ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ((,) β π) β§ π§ = (Ξ£^β((vol β (,)) β π)))} & β’ (π β π = (Ξ£^β((vol β [,)) β πΉ))) & β’ π = (Ξ£^β((vol β (,)) β πΊ)) & β’ (π β πΉ:ββΆ(β Γ β)) & β’ (π β π΄ β βͺ ran ([,) β πΉ)) & β’ (π β π β β+) & β’ πΊ = (π β β β¦ β¨((1st β(πΉβπ)) β (π / (2βπ))), (2nd β(πΉβπ))β©) β β’ (π β βπ§ β π π§ β€ (π +π π)) | ||
Theorem | ovolval5lem3 45668* | The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ π = {π¦ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ([,) β π) β§ π¦ = (Ξ£^β((vol β [,)) β π)))} & β’ π = {π§ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ((,) β π) β§ π§ = (Ξ£^β((vol β (,)) β π)))} β β’ inf(π, β*, < ) = inf(π, β*, < ) | ||
Theorem | ovolval5 45669* | The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ π = {π¦ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ([,) β π) β§ π¦ = (Ξ£^β((vol β [,)) β π)))} β β’ (π β (vol*βπ΄) = inf(π, β*, < )) | ||
Theorem | ovnovollem1 45670* | if πΉ is a cover of π΅ in β, then πΌ is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β πΉ β ((β Γ β) βm β)) & β’ πΌ = (π β β β¦ {β¨π΄, (πΉβπ)β©}) & β’ (π β π΅ β βͺ ran ([,) β πΉ)) & β’ (π β π΅ β π) & β’ (π β π = (Ξ£^β((vol β [,)) β πΉ))) β β’ (π β βπ β (((β Γ β) βm {π΄}) βm β)((π΅ βm {π΄}) β βͺ π β β Xπ β {π΄} (([,) β (πβπ))βπ) β§ π = (Ξ£^β(π β β β¦ βπ β {π΄} (volβ(([,) β (πβπ))βπ)))))) | ||
Theorem | ovnovollem2 45671* | if πΌ is a cover of (π΅ βm {π΄}) in β^1, then πΉ is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΌ β (((β Γ β) βm {π΄}) βm β)) & β’ (π β (π΅ βm {π΄}) β βͺ π β β Xπ β {π΄} (([,) β (πΌβπ))βπ)) & β’ (π β π = (Ξ£^β(π β β β¦ βπ β {π΄} (volβ(([,) β (πΌβπ))βπ))))) & β’ πΉ = (π β β β¦ ((πΌβπ)βπ΄)) β β’ (π β βπ β ((β Γ β) βm β)(π΅ β βͺ ran ([,) β π) β§ π = (Ξ£^β((vol β [,)) β π)))) | ||
Theorem | ovnovollem3 45672* | The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β β) & β’ π = {π§ β β* β£ βπ β (((β Γ β) βm {π΄}) βm β)((π΅ βm {π΄}) β βͺ π β β Xπ β {π΄} (([,) β (πβπ))βπ) β§ π§ = (Ξ£^β(π β β β¦ βπ β {π΄} (volβ(([,) β (πβπ))βπ)))))} & β’ π = {π§ β β* β£ βπ β ((β Γ β) βm β)(π΅ β βͺ ran ([,) β π) β§ π§ = (Ξ£^β((vol β [,)) β π)))} β β’ (π β ((voln*β{π΄})β(π΅ βm {π΄})) = (vol*βπ΅)) | ||
Theorem | ovnovol 45673 | The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β β) β β’ (π β ((voln*β{π΄})β(π΅ βm {π΄})) = (vol*βπ΅)) | ||
Theorem | vonvolmbllem 45674* | If a subset π΅ of real numbers is Lebesgue measurable, then its corresponding 1-dimensional set is measurable w.r.t. the n-dimensional Lebesgue measure, (with π equal to 1). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β β) & β’ (π β βπ¦ β π« β(vol*βπ¦) = ((vol*β(π¦ β© π΅)) +π (vol*β(π¦ β π΅)))) & β’ (π β π β (β βm {π΄})) & β’ π = βͺ π β π ran π β β’ (π β (((voln*β{π΄})β(π β© (π΅ βm {π΄}))) +π ((voln*β{π΄})β(π β (π΅ βm {π΄})))) = ((voln*β{π΄})βπ)) | ||
Theorem | vonvolmbl 45675 | A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β β) β β’ (π β ((π΅ βm {π΄}) β dom (volnβ{π΄}) β π΅ β dom vol)) | ||
Theorem | vonvol 45676 | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β dom vol) β β’ (π β ((volnβ{π΄})β(π΅ βm {π΄})) = (volβπ΅)) | ||
Theorem | vonvolmbl2 45677* | A subset π of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection π on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β π β (β βm {π΄})) & β’ π = βͺ π β π ran π β β’ (π β (π β dom (volnβ{π΄}) β π β dom vol)) | ||
Theorem | vonvol2 45678* | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β π β dom (volnβ{π΄})) & β’ π = βͺ π β π ran π β β’ (π β ((volnβ{π΄})βπ) = (volβπ)) | ||
Theorem | hoimbl2 45679* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Xπ β π (π΄[,)π΅) β π) | ||
Theorem | voncl 45680 | The Lebesgue measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄ β π) β β’ (π β ((volnβπ)βπ΄) β (0[,]+β)) | ||
Theorem | vonhoi 45681* | The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). A direct consequence of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) β β’ (π β ((volnβπ)βπΌ) = (π΄(πΏβπ)π΅)) | ||
Theorem | vonxrcl 45682 | The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄ β π) β β’ (π β ((volnβπ)βπ΄) β β*) | ||
Theorem | ioosshoi 45683 | A n-dimensional open interval is a subset of the half-open interval with the same bounds. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ Xπ β π (π΄(,)π΅) β Xπ β π (π΄[,)π΅) | ||
Theorem | vonn0hoi 45684* | The Lebesgue outer measure of a multidimensional half-open interval when the dimension of the space is nonzero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) β β’ (π β ((volnβπ)βπΌ) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) | ||
Theorem | von0val 45685 | The Lebesgue measure (for the zero dimensional space of reals) of every measurable set is zero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β dom (volnββ )) β β’ (π β ((volnββ )βπ΄) = 0) | ||
Theorem | vonhoire 45686* | The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β ((volnβπ)βXπ β π (π΄[,)π΅)) β β) | ||
Theorem | iinhoiicclem 45687* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β πΉ β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π)))) β β’ (π β πΉ β Xπ β π (π΄[,]π΅)) | ||
Theorem | iinhoiicc 45688* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) = Xπ β π (π΄[,]π΅)) | ||
Theorem | iunhoiioolem 45689* | A n-dimensional open interval expressed as the indexed union of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β π β β ) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β*) & β’ (π β πΉ β Xπ β π (π΄(,)π΅)) & β’ πΆ = inf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) β β’ (π β πΉ β βͺ π β β Xπ β π ((π΄ + (1 / π))[,)π΅)) | ||
Theorem | iunhoiioo 45690* | A n-dimensional open interval expressed as the indexed union of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β*) β β’ (π β βͺ π β β Xπ β π ((π΄ + (1 / π))[,)π΅) = Xπ β π (π΄(,)π΅)) | ||
Theorem | ioovonmbl 45691* | Any n-dimensional open interval is Lebesgue measurable. This is the first statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄:πβΆβ*) & β’ (π β π΅:πβΆβ*) β β’ (π β Xπ β π ((π΄βπ)(,)(π΅βπ)) β π) | ||
Theorem | iccvonmbllem 45692* | Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΆ = (π β β β¦ (π β π β¦ ((π΄βπ) β (1 / π)))) & β’ π· = (π β β β¦ (π β π β¦ ((π΅βπ) + (1 / π)))) β β’ (π β Xπ β π ((π΄βπ)[,](π΅βπ)) β π) | ||
Theorem | iccvonmbl 45693* | Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) β β’ (π β Xπ β π ((π΄βπ)[,](π΅βπ)) β π) | ||
Theorem | vonioolem1 45694* | The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β π β β ) & β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) & β’ πΆ = (π β β β¦ (π β π β¦ ((π΄βπ) + (1 / π)))) & β’ π· = (π β β β¦ Xπ β π (((πΆβπ)βπ)[,)(π΅βπ))) & β’ π = (π β β β¦ ((volnβπ)β(π·βπ))) & β’ π = (π β β β¦ βπ β π ((π΅βπ) β ((πΆβπ)βπ))) & β’ πΈ = inf(ran (π β π β¦ ((π΅βπ) β (π΄βπ))), β, < ) & β’ π = ((ββ(1 / πΈ)) + 1) & β’ π = (β€β₯βπ) β β’ (π β π β βπ β π ((π΅βπ) β (π΄βπ))) | ||
Theorem | vonioolem2 45695* | The n-dimensional Lebesgue measure of open intervals. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β π β β ) & β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) & β’ πΌ = Xπ β π ((π΄βπ)(,)(π΅βπ)) & β’ πΆ = (π β β β¦ (π β π β¦ ((π΄βπ) + (1 / π)))) & β’ π· = (π β β β¦ Xπ β π (((πΆβπ)βπ)[,)(π΅βπ))) β β’ (π β ((volnβπ)βπΌ) = βπ β π ((π΅βπ) β (π΄βπ))) | ||
Theorem | vonioo 45696* | The n-dimensional Lebesgue measure of an open interval. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)(,)(π΅βπ)) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) β β’ (π β ((volnβπ)βπΌ) = (π΄(πΏβπ)π΅)) | ||
Theorem | vonicclem1 45697* | The sequence of the measures of the half-open intervals converges to the measure of their intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β π β β ) & β’ ((π β§ π β π) β (π΄βπ) β€ (π΅βπ)) & β’ πΆ = (π β β β¦ (π β π β¦ ((π΅βπ) + (1 / π)))) & β’ π· = (π β β β¦ Xπ β π ((π΄βπ)[,)((πΆβπ)βπ))) & β’ π = (π β β β¦ ((volnβπ)β(π·βπ))) β β’ (π β π β βπ β π ((π΅βπ) β (π΄βπ))) | ||
Theorem | vonicclem2 45698* | The n-dimensional Lebesgue measure of closed intervals. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ (π β π β β ) & β’ ((π β§ π β π) β (π΄βπ) β€ (π΅βπ)) & β’ πΌ = Xπ β π ((π΄βπ)[,](π΅βπ)) & β’ πΆ = (π β β β¦ (π β π β¦ ((π΅βπ) + (1 / π)))) & β’ π· = (π β β β¦ Xπ β π ((π΄βπ)[,)((πΆβπ)βπ))) β β’ (π β ((volnβπ)βπΌ) = βπ β π ((π΅βπ) β (π΄βπ))) | ||
Theorem | vonicc 45699* | The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,](π΅βπ)) & β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β , 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) β β’ (π β ((volnβπ)βπΌ) = (π΄(πΏβπ)π΅)) | ||
Theorem | snvonmbl 45700 | A n-dimensional singleton is Lebesgue measurable. This is the first statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) β β’ (π β {π΄} β dom (volnβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |