Home | Metamath
Proof Explorer Theorem List (p. 447 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ovolval5lem1 44601* | β’ (π β (Ξ£^β(π β β β¦ (volβ((π΄ β (π / (2βπ) ))(,)π΅)))) β€ ((Ξ£^β(π β β β¦ (volβ(π΄[,)π΅) ))) +π π)). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π β§ π β β) β π΄ β β) & β’ ((π β§ π β β) β π΅ β β) & β’ (π β π β β+) & β’ πΆ = {π β β β£ π΄ < π΅} β β’ (π β (Ξ£^β(π β β β¦ (volβ((π΄ β (π / (2βπ)))(,)π΅)))) β€ ((Ξ£^β(π β β β¦ (volβ(π΄[,)π΅)))) +π π)) | ||
Theorem | ovolval5lem2 44602* | β’ ((π β§ π β β) β β¨((1st β(πΉβπ)) β (π / (2βπ))), (2nd β(πΉβπ))β© β (β Γ β)). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ π = {π§ β β* β£ βπ β ((β Γ β) βm β)(π΄ β βͺ ran ((,) β π) β§ π§ = (Ξ£^β((vol β (,)) β π)))} & β’ (π β π = (Ξ£^β((vol β [,)) β πΉ))) & β’ π = (Ξ£^β((vol β (,)) β πΊ)) & β’ (π β πΉ:ββΆ(β Γ β)) & β’ (π β π΄ β βͺ ran ([,) β πΉ)) & β’ (π β π β β+) & β’ πΊ = (π β β β¦ β¨((1st β(πΉβπ)) β (π / (2βπ))), (2nd β(πΉβπ))β©) β β’ (π β βπ§ β π π§ β€ (π +π π)) | ||
Theorem | ovolval5lem3 44603* | 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 44604* | 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 44605* | 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 44606* | 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 44607* | 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 44608 | 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 44609* | 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 44610 | 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 44611 | 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 44612* | 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 44613* | 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 44614* | 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 44615 | 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 44616* | 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 44617 | The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ π = dom (volnβπ) & β’ (π β π΄ β π) β β’ (π β ((volnβπ)βπ΄) β β*) | ||
Theorem | ioosshoi 44618 | 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 44619* | 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 44620 | 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 44621* | 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 44622* | 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 44623* | 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 44624* | 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 44625* | 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 44626* | 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 44627* | 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 44628* | 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 44629* | 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 44630* | 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 44631* | 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 44632* | 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 44633* | 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 44634* | 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 44635 | 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βπ)) | ||
Theorem | vonn0ioo 44636* | The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)(,)(π΅βπ)) β β’ (π β ((volnβπ)βπΌ) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) | ||
Theorem | vonn0icc 44637* | The n-dimensional Lebesgue measure of a closed interval, when the dimension of the space is nonzero. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π΄:πβΆβ) & β’ (π β π΅:πβΆβ) & β’ πΌ = Xπ β π ((π΄βπ)[,](π΅βπ)) β β’ (π β ((volnβπ)βπΌ) = βπ β π (volβ((π΄βπ)[,](π΅βπ)))) | ||
Theorem | ctvonmbl 44638 | Any n-dimensional countable set is Lebesgue measurable. This is the second statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ (π β π΄ βΌ Ο) β β’ (π β π΄ β dom (volnβπ)) | ||
Theorem | vonn0ioo2 44639* | The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β π β β ) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) & β’ πΌ = Xπ β π (π΄(,)π΅) β β’ (π β ((volnβπ)βπΌ) = βπ β π (volβ(π΄(,)π΅))) | ||
Theorem | vonsn 44640 | The n-dimensional Lebesgue measure of a singleton is zero. This is the first statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) β β’ (π β ((volnβπ)β{π΄}) = 0) | ||
Theorem | vonn0icc2 44641* | The n-dimensional Lebesgue measure of a closed interval, when the dimension of the space is nonzero. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ (π β π β β ) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) & β’ πΌ = Xπ β π (π΄[,]π΅) β β’ (π β ((volnβπ)βπΌ) = βπ β π (volβ(π΄[,]π΅))) | ||
Theorem | vonct 44642 | The n-dimensional Lebesgue measure of any countable set is zero. This is the second statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄ β (β βm π)) & β’ (π β π΄ βΌ Ο) β β’ (π β ((volnβπ)βπ΄) = 0) | ||
Theorem | vitali2 44643 | There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 10365). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ dom vol β π« β | ||
Proofs for most of the theorems in section 121 of [Fremlin1]. Real-valued functions are considered, and measurability is defined with respect to an arbitrary sigma-algebra. When the sigma-algebra on the domain is the Lebesgue measure on the reals, then all real-valued measurable functions in the sense of df-mbf 24905 are also sigma-measurable, but the definition in this section considers as measurable functions, some that are not measurable in the sense of df-mbf 24905 (see mbfpsssmf 44732 and smfmbfcex 44709). | ||
Syntax | csmblfn 44644 | Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras. |
class SMblFn | ||
Definition | df-smblfn 44645* | Define a real-valued measurable function w.r.t. a given sigma-algebra. See Definition 121C of [Fremlin1] p. 36 and Definition 135E (b) of [Fremlin1] p. 80 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ SMblFn = (π β SAlg β¦ {π β (β βpm βͺ π ) β£ βπ β β (β‘π β (-β(,)π)) β (π βΎt dom π)}) | ||
Theorem | pimltmnf2f 44646 | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -β, is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2024.) |
β’ β²π₯πΉ & β’ β²π₯π΄ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ (πΉβπ₯) < -β} = β ) | ||
Theorem | pimltmnf2 44647* | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -β, is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ (πΉβπ₯) < -β} = β ) | ||
Theorem | preimagelt 44648* | The preimage of a right-open, unbounded below interval, is the complement of a left-closed unbounded above interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β*) β β’ (π β (π΄ β {π₯ β π΄ β£ πΆ β€ π΅}) = {π₯ β π΄ β£ π΅ < πΆ}) | ||
Theorem | preimalegt 44649* | The preimage of a left-open, unbounded above interval, is the complement of a right-closed unbounded below interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β*) β β’ (π β (π΄ β {π₯ β π΄ β£ π΅ β€ πΆ}) = {π₯ β π΄ β£ πΆ < π΅}) | ||
Theorem | pimconstlt0 44650* | Given a constant function, its preimage with respect to an unbounded below, open interval, with upper bound less than or equal to the constant, is the empty set. Second part of Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π΅ β β) & β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β πΆ β β*) & β’ (π β πΆ β€ π΅) β β’ (π β {π₯ β π΄ β£ (πΉβπ₯) < πΆ} = β ) | ||
Theorem | pimconstlt1 44651* | Given a constant function, its preimage with respect to an unbounded below, open interval, with upper bound larger than the constant, is the whole domain. First part of Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π΅ β β) & β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β π΅ < πΆ) β β’ (π β {π₯ β π΄ β£ (πΉβπ₯) < πΆ} = π΄) | ||
Theorem | pimltpnff 44652 | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +β, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β {π₯ β π΄ β£ π΅ < +β} = π΄) | ||
Theorem | pimltpnf 44653* | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +β, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β {π₯ β π΄ β£ π΅ < +β} = π΄) | ||
Theorem | pimgtpnf2f 44654 | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +β, is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2021.) |
β’ β²π₯πΉ & β’ β²π₯π΄ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ +β < (πΉβπ₯)} = β ) | ||
Theorem | pimgtpnf2 44655* | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +β, is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ +β < (πΉβπ₯)} = β ) | ||
Theorem | salpreimagelt 44656* | If all the preimages of left-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (iv) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π΄ = βͺ π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π β€ π΅} β π) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ π΅ < πΆ} β π) | ||
Theorem | pimrecltpos 44657 | The preimage of an unbounded below, open interval, with positive upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β π΅ β 0) & β’ (π β πΆ β β+) β β’ (π β {π₯ β π΄ β£ (1 / π΅) < πΆ} = ({π₯ β π΄ β£ (1 / πΆ) < π΅} βͺ {π₯ β π΄ β£ π΅ < 0})) | ||
Theorem | salpreimalegt 44658* | If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of left-open, unbounded above intervals, belong to the sigma-algebra. (ii) implies (iii) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π΄ = βͺ π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π΅ β€ π} β π) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ πΆ < π΅} β π) | ||
Theorem | pimiooltgt 44659* | The preimage of an open interval is the intersection of the preimage of an unbounded below open interval and an unbounded above open interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β πΏ β β*) & β’ (π β π β β*) & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β {π₯ β π΄ β£ π΅ β (πΏ(,)π )} = ({π₯ β π΄ β£ π΅ < π } β© {π₯ β π΄ β£ πΏ < π΅})) | ||
Theorem | preimaicomnf 44660* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ*) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | pimltpnf2f 44661 | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +β, is the whole domain. (Contributed by Glauco Siliprandi, 15-Dec-2024.) |
β’ β²π₯πΉ & β’ β²π₯π΄ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ (πΉβπ₯) < +β} = π΄) | ||
Theorem | pimltpnf2 44662* | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +β, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ (πΉβπ₯) < +β} = π΄) | ||
Theorem | pimgtmnf2 44663* | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -β, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆβ) β β’ (π β {π₯ β π΄ β£ -β < (πΉβπ₯)} = π΄) | ||
Theorem | pimdecfgtioc 44664* | Given a nonincreasing function, the preimage of an unbounded above, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) & β’ (π β π β β*) & β’ π = {π₯ β π΄ β£ π < (πΉβπ₯)} & β’ π = sup(π, β*, < ) & β’ (π β π β π) & β’ πΌ = (-β(,]π) β β’ (π β π = (πΌ β© π΄)) | ||
Theorem | pimincfltioc 44665* | Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) & β’ (π β π β β*) & β’ π = {π₯ β π΄ β£ (πΉβπ₯) < π } & β’ π = sup(π, β*, < ) & β’ (π β π β π) & β’ πΌ = (-β(,]π) β β’ (π β π = (πΌ β© π΄)) | ||
Theorem | pimdecfgtioo 44666* | Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage does not belong to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) & β’ (π β π β β*) & β’ π = {π₯ β π΄ β£ π < (πΉβπ₯)} & β’ π = sup(π, β*, < ) & β’ (π β Β¬ π β π) & β’ πΌ = (-β(,)π) β β’ (π β π = (πΌ β© π΄)) | ||
Theorem | pimincfltioo 44667* | Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage does not belong to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) & β’ (π β π β β*) & β’ π = {π₯ β π΄ β£ (πΉβπ₯) < π } & β’ π = sup(π, β*, < ) & β’ (π β Β¬ π β π) & β’ πΌ = (-β(,)π) β β’ (π β π = (πΌ β© π΄)) | ||
Theorem | preimaioomnf 44668* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | preimageiingt 44669* | A preimage of a left-closed, unbounded above interval, expressed as an indexed intersection of preimages of open, unbounded above intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ πΆ β€ π΅} = β© π β β {π₯ β π΄ β£ (πΆ β (1 / π)) < π΅}) | ||
Theorem | preimaleiinlt 44670* | A preimage of a left-open, right-closed, unbounded below interval, expressed as an indexed intersection of preimages of open, unbound below intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ π΅ β€ πΆ} = β© π β β {π₯ β π΄ β£ π΅ < (πΆ + (1 / π))}) | ||
Theorem | pimgtmnff 44671 | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -β, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β {π₯ β π΄ β£ -β < π΅} = π΄) | ||
Theorem | pimgtmnf 44672* | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -β, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β {π₯ β π΄ β£ -β < π΅} = π΄) | ||
Theorem | pimrecltneg 44673 | The preimage of an unbounded below, open interval, with negative upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β π΅ β 0) & β’ (π β πΆ β β) & β’ (π β πΆ < 0) β β’ (π β {π₯ β π΄ β£ (1 / π΅) < πΆ} = {π₯ β π΄ β£ π΅ β ((1 / πΆ)(,)0)}) | ||
Theorem | salpreimagtge 44674* | If all the preimages of left-open, unbounded above intervals, belong to a sigma-algebra, then all the preimages of left-closed, unbounded above intervals, belong to the sigma-algebra. (iii) implies (iv) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π < π΅} β π) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ πΆ β€ π΅} β π) | ||
Theorem | salpreimaltle 44675* | If all the preimages of right-open, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-closed, unbounded below intervals, belong to the sigma-algebra. (i) implies (ii) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π΅ < π} β π) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ π΅ β€ πΆ} β π) | ||
Theorem | issmflem 44676* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of πΉ is required to be a subset of the underlying set of π. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ π· = dom πΉ β β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)))) | ||
Theorem | issmf 44677* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of πΉ is required to be a subset of the underlying set of π. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ π· = dom πΉ β β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)))) | ||
Theorem | salpreimalelt 44678* | If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (ii) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π΄ = βͺ π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π΅ β€ π} β π) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ π΅ < πΆ} β π) | ||
Theorem | salpreimagtlt 44679* | If all the preimages of lef-open, unbounded above intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (iii) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π΄ = βͺ π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π < π΅} β π) & β’ (π β πΆ β β) β β’ (π β {π₯ β π΄ β£ π΅ < πΆ} β π) | ||
Theorem | smfpreimalt 44680* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β) β β’ (π β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) | ||
Theorem | smff 44681 | A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ β β’ (π β πΉ:π·βΆβ) | ||
Theorem | smfdmss 44682 | The domain of a function measurable w.r.t. to a sigma-algebra, is a subset of the set underlying the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ β β’ (π β π· β βͺ π) | ||
Theorem | issmff 44683* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of πΉ is required to be a subset of the underlying set of π. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ π· = dom πΉ β β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)))) | ||
Theorem | issmfd 44684* | A sufficient condition for "πΉ being a real-valued measurable function w.r.t. to the sigma-algebra π". (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²ππ & β’ (π β π β SAlg) & β’ (π β π· β βͺ π) & β’ (π β πΉ:π·βΆβ) & β’ ((π β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | smfpreimaltf 44685* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β) β β’ (π β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) | ||
Theorem | issmfdf 44686* | A sufficient condition for "πΉ being a measurable function w.r.t. to the sigma-algebra π". (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯πΉ & β’ β²ππ & β’ (π β π β SAlg) & β’ (π β π· β βͺ π) & β’ (π β πΉ:π·βΆβ) & β’ ((π β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | sssmf 44687 | The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) β β’ (π β (πΉ βΎ π΅) β (SMblFnβπ)) | ||
Theorem | mbfresmf 44688 | A real-valued measurable function is a sigma-measurable function (w.r.t. the Lebesgue measure on the Reals). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ β MblFn) & β’ (π β ran πΉ β β) & β’ π = dom vol β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | cnfsmf 44689 | A continuous function is measurable. Proposition 121D (b) of [Fremlin1] p. 36 is a special case of this theorem, where the topology on the domain is induced by the standard topology on n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π½ β Top) & β’ πΎ = (topGenβran (,)) & β’ (π β πΉ β ((π½ βΎt dom πΉ) Cn πΎ)) & β’ π = (SalGenβπ½) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | incsmflem 44690* | A nondecreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π β β*) & β’ π = {π₯ β π΄ β£ (πΉβπ₯) < π } & β’ πΆ = sup(π, β*, < ) & β’ π· = (-β(,)πΆ) & β’ πΈ = (-β(,]πΆ) β β’ (π β βπ β π΅ π = (π β© π΄)) | ||
Theorem | incsmf 44691* | A real-valued, nondecreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π β πΉ β (SMblFnβπ΅)) | ||
Theorem | smfsssmf 44692 | If a function is measurable w.r.t. to a sigma-algebra, then it is measurable w.r.t. to a larger sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π β SAlg) & β’ (π β π β π) & β’ (π β πΉ β (SMblFnβπ )) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | issmflelem 44693* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of πΉ is required to be a subset of the underlying set of π. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (ii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π· = dom πΉ & β’ (π β π· β βͺ π) & β’ (π β πΉ:π·βΆβ) & β’ ((π β§ π β β) β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·)) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | issmfle 44694* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of πΉ is required to be b subset of the underlying set of π. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (ii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ π· = dom πΉ β β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·)))) | ||
Theorem | smfpimltmpt 44695* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β π β β) β β’ (π β {π₯ β π΄ β£ π΅ < π } β (π βΎt π΄)) | ||
Theorem | smfpimltxr 44696* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.) |
β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β*) β β’ (π β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) | ||
Theorem | issmfdmpt 44697* | A sufficient condition for "πΉ being a measurable function w.r.t. to the sigma-algebra π". (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ (π β π΄ β βͺ π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π β β) β {π₯ β π΄ β£ π΅ < π} β (π βΎt π΄)) β β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) | ||
Theorem | smfconst 44698* | Given a sigma-algebra over a base set X, every partial real-valued constant function is measurable. Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β βͺ π) & β’ (π β π΅ β β) & β’ πΉ = (π₯ β π΄ β¦ π΅) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | sssmfmpt 44699* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΆ β π΄) β β’ (π β (π₯ β πΆ β¦ π΅) β (SMblFnβπ)) | ||
Theorem | cnfrrnsmf 44700 | A function, continuous from the standard topology on the space of n-dimensional reals to the standard topology on the reals, is Borel measurable. Proposition 121D (b) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β Fin) & β’ π½ = (TopOpenβ(β^βπ)) & β’ πΎ = (topGenβran (,)) & β’ (π β πΉ β ((π½ βΎt dom πΉ) Cn πΎ)) & β’ π΅ = (SalGenβπ½) β β’ (π β πΉ β (SMblFnβπ΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |