![]() |
Metamath
Proof Explorer Theorem List (p. 458 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vonn0ioo 45701* | 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 45702* | 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 45703 | 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 45704* | 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 45705 | 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 45706* | 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 45707 | 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 45708 | There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 10492). (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 25368 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 25368 (see mbfpsssmf 45797 and smfmbfcex 45774). | ||
Syntax | csmblfn 45709 | Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras. |
class SMblFn | ||
Definition | df-smblfn 45710* | 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 45711 | 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 45712* | 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 45713* | 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 45714* | 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 45715* | 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 45716* | 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 45717 | 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 45718* | 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 45719 | 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 45720* | 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 45721* | 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 45722 | 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 45723* | 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 45724* | 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 45725* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ*) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | pimltpnf2f 45726 | 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 45727* | 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 45728* | 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 45729* | 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 45730* | 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 45731* | 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 45732* | 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 45733* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | preimageiingt 45734* | 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 45735* | 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 45736 | 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 45737* | 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 45738 | 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 45739* | 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 45740* | 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 45741* | 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 45742* | 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 45743* | 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 45744* | 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 45745* | 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 45746 | 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 45747 | 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 45748* | 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 45749* | 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 45750* | 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 45751* | 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 45752 | The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) β β’ (π β (πΉ βΎ π΅) β (SMblFnβπ)) | ||
Theorem | mbfresmf 45753 | 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 45754 | 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 45755* | 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 45756* | 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 45757 | 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 45758* | 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 45759* | 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 45760* | 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 45761* | 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 45762* | 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 45763* | 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 45764* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΆ β π΄) β β’ (π β (π₯ β πΆ β¦ π΅) β (SMblFnβπ)) | ||
Theorem | cnfrrnsmf 45765 | 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 45766* | The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π΄ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (SMblFnβπ΅)) | ||
Theorem | bormflebmf 45767 | 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 45768* | 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 45769* | 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 45770* | 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 45771* | 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 45772* | 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 45773* | 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 45774* | 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 25368). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = dom vol & β’ (π β π β β) & β’ (π β Β¬ π β π) & β’ πΉ = (π₯ β π β¦ 0) β β’ (π β (πΉ β (SMblFnβπ) β§ Β¬ πΉ β MblFn)) | ||
Theorem | issmfgtd 45775* | 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 45776* | 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 45777* | 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 45778* | 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 45779* | 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 45780* | 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 45781* | 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 45782* | 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 45783* | 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 45784* | 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 45785* | 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 45786* | 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 45787* | 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 45788* | 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 45789* | 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 45790* | 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 45791* | 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 45792* | 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 45793 | 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 45794* | 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 45795* | 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 45796* | 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 45797 | 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 45798* | 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 π΄)) | ||
Theorem | smfpimgtxrmpt 45799* | 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, 20-Dec-2024.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΏ β β*) β β’ (π β {π₯ β π΄ β£ πΏ < π΅} β (π βΎt π΄)) | ||
Theorem | smfpimioompt 45800* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΏ β β*) & β’ (π β π β β*) β β’ (π β {π₯ β π΄ β£ π΅ β (πΏ(,)π )} β (π βΎt π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |