Home | Metamath
Proof Explorer Theorem List (p. 409 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hoidmvval0 40801* | The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Theorem | hoiprodp1 40802* | The dimensional volume of a half-open interval with dimension . Used in the first equality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Theorem | sge0hsphoire 40803* | 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.) |
Σ^ Σ^ | ||
Theorem | hoidmvval0b 40804* | The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Theorem | hoidmv1lelem1 40805* | 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.) |
Σ^ Σ^ | ||
Theorem | hoidmv1lelem2 40806* | 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.) |
Σ^ Σ^ | ||
Theorem | hoidmv1lelem3 40807* | 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 non-empty, finite generalized sum, sub case in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | hoidmv1le 40808* | 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.) |
Σ^ | ||
Theorem | hoidmvlelem1 40809* | The supremum of belongs to . Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ Σ^ | ||
Theorem | hoidmvlelem2 40810* | 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.) |
Σ^ Σ^ inf | ||
Theorem | hoidmvlelem3 40811* | 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.) |
Σ^ Σ^ Σ^ | ||
Theorem | hoidmvlelem4 40812* | 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 . (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ Σ^ Σ^ Σ^ | ||
Theorem | hoidmvlelem5 40813* | 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.) |
Σ^ Σ^ | ||
Theorem | hoidmvle 40814* | 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.) |
Σ^ | ||
Theorem | ovnhoilem1 40815* | 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.) |
Σ^ voln* | ||
Theorem | ovnhoilem2 40816* | 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.) |
Σ^ voln* | ||
Theorem | ovnhoi 40817* | 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.) |
voln* | ||
Theorem | dmovn 40818 | 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.) |
voln* | ||
Theorem | hoicoto2 40819* | 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.) |
Theorem | dmvon 40820 | Lebesgue measurable n-dimensional subsets of Reals. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
voln CaraGenvoln* | ||
Theorem | hoi2toco 40821* | 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.) |
Theorem | hoidifhspval 40822* | 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.) |
Theorem | hspval 40823* | The value of the half-space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
Theorem | ovnlecvr2 40824* | 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.) |
voln* Σ^ | ||
Theorem | ovncvr2 40825* | 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.) |
Σ^ voln* Σ^ voln* | ||
Theorem | dmovnsal 40826 | The domain of the Lebesgue measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
voln SAlg | ||
Theorem | unidmovn 40827 | Base set of the n-dimensional Lebesgue outer measure (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
voln* | ||
Theorem | rrnmbl 40828 | The set of n-dimensional Real numbers is Lebesgue measurable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
voln | ||
Theorem | hoidifhspval2 40829* | 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.) |
Theorem | hspdifhsp 40830* | 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.) |
Theorem | unidmvon 40831 | Base set of the n-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
voln | ||
Theorem | hoidifhspf 40832* | 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.) |
Theorem | hoidifhspval3 40833* | 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.) |
Theorem | hoidifhspdmvle 40834* | 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.) |
Theorem | voncmpl 40835 | 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.) |
voln voln voln | ||
Theorem | hoiqssbllem1 40836* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
Theorem | hoiqssbllem2 40837* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
ℝ^ | ||
Theorem | hoiqssbllem3 40838* | A n-dimensional ball contains a non-empty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
ℝ^ | ||
Theorem | hoiqssbl 40839* | A n-dimensional ball contains a non-empty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
ℝ^ | ||
Theorem | hspmbllem1 40840* | 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.) |
Theorem | hspmbllem2 40841* | 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.) |
Σ^ voln* voln* voln* voln* voln* voln* voln* | ||
Theorem | hspmbllem3 40842* | 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.) |
voln* Σ^ voln* voln* voln* voln* | ||
Theorem | hspmbl 40843* | 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.) |
voln | ||
Theorem | hoimbllem 40844* | 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.) |
voln | ||
Theorem | hoimbl 40845* | 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.) |
voln | ||
Theorem | opnvonmbllem1 40846* | The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
Theorem | opnvonmbllem2 40847* | 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.) |
voln ℝ^ | ||
Theorem | opnvonmbl 40848 | 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.) |
voln ℝ^ | ||
Theorem | opnssborel 40849 | 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.) |
ℝ^ SalGen | ||
Theorem | borelmbl 40850 | 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.) |
voln SalGenℝ^ | ||
Theorem | volicorege0 40851 | 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.) |
Theorem | isvonmbl 40852* | 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.) |
voln voln* voln* voln* | ||
Theorem | mblvon 40853 | 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.) |
voln voln voln* | ||
Theorem | vonmblss 40854 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
voln | ||
Theorem | volico2 40855 | The measure of left closed, right open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Theorem | vonmblss2 40856 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
voln | ||
Theorem | ovolval2lem 40857* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Theorem | ovolval2 40858* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. See ovolval 23242 for an alternative expression. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ inf | ||
Theorem | ovnsubadd2lem 40859* | 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.) |
voln* voln*voln* | ||
Theorem | ovnsubadd2 40860 | 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.) |
voln* voln*voln* | ||
Theorem | ovolval3 40861* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^ and . See ovolval 23242 and ovolval2 40858 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ inf | ||
Theorem | ovnsplit 40862 | 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.) |
voln* voln* voln* | ||
Theorem | ovolval4lem1 40863* | |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Theorem | ovolval4lem2 40864* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 40861, but here is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ inf | ||
Theorem | ovolval4 40865* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 40861, but here may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ inf | ||
Theorem | ovolval5lem1 40866* | |- ( ph -> ( sum^ ( ( A - ( W / ( 2 ^ n ) ) ) (,) B ) ) ) ) <_ ( ( sum^ ( A [,) B ) ) ) ) +e W ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ Σ^ | ||
Theorem | ovolval5lem2 40867* | |- ( ( ph /\ n e. NN ) -> <. ( ( 1st n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd n ) ) >. e. ( RR X. RR ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ Σ^ Σ^ | ||
Theorem | ovolval5lem3 40868* | 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.) |
Σ^ Σ^ inf inf | ||
Theorem | ovolval5 40869* | 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.) |
Σ^ inf | ||
Theorem | ovnovollem1 40870* | 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.) |
Σ^ Σ^ | ||
Theorem | ovnovollem2 40871* | if is a cover of in ℝ^, then is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ Σ^ | ||
Theorem | ovnovollem3 40872* | 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* | ||
Theorem | ovnovol 40873 | 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* | ||
Theorem | vonvolmbllem 40874* | 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 ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
voln* voln* voln* | ||
Theorem | vonvolmbl 40875 | 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.) |
voln | ||
Theorem | vonvol 40876 | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
voln | ||
Theorem | vonvolmbl2 40877* | 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.) |
voln | ||
Theorem | vonvol2 40878* | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
voln voln | ||
Theorem | hoimbl2 40879* | 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.) |
voln | ||
Theorem | voncl 40880 | The Lebesgue measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
voln voln | ||
Theorem | vonhoi 40881* | 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.) |
voln | ||
Theorem | vonxrcl 40882 | The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
voln voln | ||
Theorem | ioosshoi 40883 | A n-dimensional open interval is a subset of the half-open interval with the same bounds. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Theorem | vonn0hoi 40884* | 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.) |
voln | ||
Theorem | von0val 40885 | The Lebesgue measure (for the zero dimensional space of reals) of every measurable set is zero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
voln voln | ||
Theorem | vonhoire 40886* | The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
voln | ||
Theorem | iinhoiicclem 40887* | 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.) |
Theorem | iinhoiicc 40888* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Theorem | iunhoiioolem 40889* | 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.) |
inf | ||
Theorem | iunhoiioo 40890* | A n-dimensional open interval expressed as the indexed union of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Theorem | ioovonmbl 40891* | 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.) |
voln | ||
Theorem | iccvonmbllem 40892* | 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.) |
voln | ||
Theorem | iccvonmbl 40893* | 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.) |
voln | ||
Theorem | vonioolem1 40894* | The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
voln inf | ||
Theorem | vonioolem2 40895* | 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.) |
voln | ||
Theorem | vonioo 40896* | 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.) |
voln | ||
Theorem | vonicclem1 40897* | The sequence of the measures of the half-open intervals converges to the measure of their intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
voln | ||
Theorem | vonicclem2 40898* | 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.) |
voln | ||
Theorem | vonicc 40899* | 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.) |
voln | ||
Theorem | snvonmbl 40900 | 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.) |
voln |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |