![]() |
Metamath
Proof Explorer Theorem List (p. 455 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vonicc 45401* | 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 45402 | 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 45403* | 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 45404* | 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 45405 | 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 45406* | 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 45407 | 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 45408* | 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 45409 | 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 45410 | There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 10490). (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 25136 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 25136 (see mbfpsssmf 45499 and smfmbfcex 45476). | ||
Syntax | csmblfn 45411 | Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras. |
class SMblFn | ||
Definition | df-smblfn 45412* | 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 45413 | 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 45414* | 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 45415* | 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 45416* | 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 45417* | 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 45418* | 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 45419 | 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 45420* | 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 45421 | 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 45422* | 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 45423* | 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 45424 | 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 45425* | 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 45426* | 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 45427* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ*) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | pimltpnf2f 45428 | 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 45429* | 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 45430* | 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 45431* | 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 45432* | 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 45433* | 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 45434* | 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 45435* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | preimageiingt 45436* | 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 45437* | 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 45438 | 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 45439* | 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 45440 | 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 45441* | 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 45442* | 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 45443* | 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 45444* | 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 45445* | 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 45446* | 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 45447* | 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 45448 | 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 45449 | 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 45450* | 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 45451* | 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 45452* | 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 45453* | 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 45454 | The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) β β’ (π β (πΉ βΎ π΅) β (SMblFnβπ)) | ||
Theorem | mbfresmf 45455 | 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 45456 | 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 45457* | 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 45458* | 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 45459 | 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 45460* | 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 45461* | 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 45462* | 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 45463* | 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 45464* | 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 45465* | 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 45466* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΆ β π΄) β β’ (π β (π₯ β πΆ β¦ π΅) β (SMblFnβπ)) | ||
Theorem | cnfrrnsmf 45467 | 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βπ΅)) | ||
Theorem | smfid 45468* | The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π΄ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (SMblFnβπ΅)) | ||
Theorem | bormflebmf 45469 | A Borel measurable function is Lebesgue measurable. Proposition 121D (a) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β Fin) & β’ π΅ = (SalGenβ(TopOpenβ(β^βπ))) & β’ πΏ = dom (volnβπ) & β’ (π β πΉ β (SMblFnβπ΅)) β β’ (π β πΉ β (SMblFnβπΏ)) | ||
Theorem | smfpreimale 45470* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded below is in the subspace sigma-algebra induced by its domain. See Proposition 121B (ii) of [Fremlin1] p. 35 (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β) β β’ (π β {π₯ β π· β£ (πΉβπ₯) β€ π΄} β (π βΎt π·)) | ||
Theorem | issmfgtlem 45471* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all left-open intervals unbounded above 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 (iii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π· = dom πΉ & β’ (π β π· β βͺ π) & β’ (π β πΉ:π·βΆβ) & β’ (π β βπ β β {π₯ β π· β£ π < (πΉβπ₯)} β (π βΎt π·)) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | issmfgt 45472* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all left-open intervals unbounded above 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 (iii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ π· = dom πΉ β β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ π < (πΉβπ₯)} β (π βΎt π·)))) | ||
Theorem | issmfled 45473* | 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 | smfpimltxrmptf 45474* | 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, 20-Dec-2024.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β π β β*) β β’ (π β {π₯ β π΄ β£ π΅ < π } β (π βΎt π΄)) | ||
Theorem | smfpimltxrmpt 45475* | 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, 20-Dec-2024.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β π β β*) β β’ (π β {π₯ β π΄ β£ π΅ < π } β (π βΎt π΄)) | ||
Theorem | smfmbfcex 45476* | A constant function, with non-lebesgue-measurable domain is a sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) but it is not a measurable functions ( w.r.t. to df-mbf 25136). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = dom vol & β’ (π β π β β) & β’ (π β Β¬ π β π) & β’ πΉ = (π₯ β π β¦ 0) β β’ (π β (πΉ β (SMblFnβπ) β§ Β¬ πΉ β MblFn)) | ||
Theorem | issmfgtd 45477* | 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 | smfpreimagt 45478* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β) β β’ (π β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) | ||
Theorem | smfaddlem1 45479* | Given the sum of two functions, the preimage of an unbounded below, open interval, expressed as the countable union of intersections of preimages of both functions. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β π β β) & β’ πΎ = (π β β β¦ {π β β β£ (π + π) < π }) β β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ + π·) < π } = βͺ π β β βͺ π β (πΎβπ){π₯ β (π΄ β© πΆ) β£ (π΅ < π β§ π· < π)}) | ||
Theorem | smfaddlem2 45480* | The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) & β’ (π β π β β) & β’ πΎ = (π β β β¦ {π β β β£ (π + π) < π }) β β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ + π·) < π } β (π βΎt (π΄ β© πΆ))) | ||
Theorem | smfadd 45481* | The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) β β’ (π β (π₯ β (π΄ β© πΆ) β¦ (π΅ + π·)) β (SMblFnβπ)) | ||
Theorem | decsmflem 45482* | A nonincreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π β β*) & β’ π = {π₯ β π΄ β£ π < (πΉβπ₯)} & β’ πΆ = sup(π, β*, < ) & β’ π· = (-β(,)πΆ) & β’ πΈ = (-β(,]πΆ) β β’ (π β βπ β π΅ π = (π β© π΄)) | ||
Theorem | decsmf 45483* | A real-valued, nonincreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (πΉβπ₯))) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π β πΉ β (SMblFnβπ΅)) | ||
Theorem | smfpreimagtf 45484* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β) β β’ (π β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) | ||
Theorem | issmfgelem 45485* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all left-closed intervals unbounded above 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 (iv) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ β²ππ & β’ (π β π β SAlg) & β’ π· = dom πΉ & β’ (π β π· β βͺ π) & β’ (π β πΉ:π·βΆβ) & β’ (π β βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·)) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | issmfge 45486* | The predicate "πΉ is a real-valued measurable function w.r.t. to the sigma-algebra π". A function is measurable iff the preimages of all left-closed intervals unbounded above 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 (iv) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ π· = dom πΉ β β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·)))) | ||
Theorem | smflimlem1 45487* | Lemma for the proof that the limit of a sequence of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that (π· β© πΌ) is in the subspace sigma-algebra induced by π·. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) & β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) & β’ πΌ = β© π β β βͺ π β π β© π β (β€β₯βπ)(ππ»π) & β’ ((π β§ π β ran π) β (πΆβπ) β π) β β’ (π β (π· β© πΌ) β (π βΎt π·)) | ||
Theorem | smflimlem2 45488* | Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by π·. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) & β’ (π β π΄ β β) & β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) & β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) & β’ πΌ = β© π β β βͺ π β π β© π β (β€β₯βπ)(ππ»π) & β’ ((π β§ π β ran π) β (πΆβπ) β π) β β’ (π β {π₯ β π· β£ (πΊβπ₯) β€ π΄} β (π· β© πΌ)) | ||
Theorem | smflimlem3 45489* | The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ (π β π΄ β β) & β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) & β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) & β’ πΌ = β© π β β βͺ π β π β© π β (β€β₯βπ)(ππ»π) & β’ ((π β§ π¦ β ran π) β (πΆβπ¦) β π¦) & β’ (π β π β (π· β© πΌ)) & β’ (π β πΎ β β) & β’ (π β π β β+) & β’ (π β (1 / πΎ) < π) β β’ (π β βπ β π βπ β (β€β₯βπ)(π β dom (πΉβπ) β§ ((πΉβπ)βπ) < (π΄ + π))) | ||
Theorem | smflimlem4 45490* | Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by π·. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) & β’ (π β π΄ β β) & β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) & β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) & β’ πΌ = β© π β β βͺ π β π β© π β (β€β₯βπ)(ππ»π) & β’ ((π β§ π β ran π) β (πΆβπ) β π) β β’ (π β (π· β© πΌ) β {π₯ β π· β£ (πΊβπ₯) β€ π΄}) | ||
Theorem | smflimlem5 45491* | Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by π·. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) & β’ (π β π΄ β β) & β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) & β’ π» = (π β π, π β β β¦ (πΆβ(πππ))) & β’ πΌ = β© π β β βͺ π β π β© π β (β€β₯βπ)(ππ»π) & β’ ((π β§ π β ran π) β (πΆβπ) β π) β β’ (π β {π₯ β π· β£ (πΊβπ₯) β€ π΄} β (π βΎt π·)) | ||
Theorem | smflimlem6 45492* | Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by π·. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) & β’ (π β π΄ β β) & β’ π = (π β π, π β β β¦ {π β π β£ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < (π΄ + (1 / π))} = (π β© dom (πΉβπ))}) β β’ (π β {π₯ β π· β£ (πΊβπ₯) β€ π΄} β (π βΎt π·)) | ||
Theorem | smflim 45493* | The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | nsssmfmbflem 45494* | The sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) are not a subset of the measurable functions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = dom vol & β’ (π β π β β) & β’ (π β Β¬ π β π) & β’ πΉ = (π₯ β π β¦ 0) β β’ (π β βπ(π β (SMblFnβπ) β§ Β¬ π β MblFn)) | ||
Theorem | nsssmfmbf 45495 | The sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) are not a subset of the measurable functions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = dom vol β β’ Β¬ (SMblFnβπ) β MblFn | ||
Theorem | smfpimgtxr 45496* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above 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 | smfpimgtmpt 45497* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΏ β β) β β’ (π β {π₯ β π΄ β£ πΏ < π΅} β (π βΎt π΄)) | ||
Theorem | smfpreimage 45498* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β) β β’ (π β {π₯ β π· β£ π΄ β€ (πΉβπ₯)} β (π βΎt π·)) | ||
Theorem | mbfpsssmf 45499 | Real-valued measurable functions are a proper subset of sigma-measurable functions (w.r.t. the Lebesgue measure on the reals). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = dom vol β β’ (MblFn β© (β βpm β)) β (SMblFnβπ) | ||
Theorem | smfpimgtxrmptf 45500* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΏ β β*) β β’ (π β {π₯ β π΄ β£ πΏ < π΅} β (π βΎt π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |