![]() |
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-30158) |
![]() (30159-31681) |
![]() (31682-47805) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | preimagelt 45401* | 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 45402* | 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 45403* | 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 45404* | 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 45405 | 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 45406* | 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 45407 | 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 45408* | 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 45409* | 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 45410 | 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 45411* | 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 45412* | 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 45413* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ*) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β[,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | pimltpnf2f 45414 | 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 45415* | 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 45416* | 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 45417* | 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 45418* | 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 45419* | 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 45420* | 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 45421* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,)π΅)) = {π₯ β π΄ β£ (πΉβπ₯) < π΅}) | ||
Theorem | preimageiingt 45422* | 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 45423* | 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 45424 | 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 45425* | 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 45426 | 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 45427* | 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 45428* | 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 45429* | 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 45430* | 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 45431* | 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 45432* | 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 45433* | 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 45434 | 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 45435 | 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 45436* | 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 45437* | 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 45438* | 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 45439* | 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 45440 | The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) β β’ (π β (πΉ βΎ π΅) β (SMblFnβπ)) | ||
Theorem | mbfresmf 45441 | 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 45442 | 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 45443* | 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 45444* | 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 45445 | 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 45446* | 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 45447* | 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 45448* | 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 45449* | 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 45450* | 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 45451* | 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 45452* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΆ β π΄) β β’ (π β (π₯ β πΆ β¦ π΅) β (SMblFnβπ)) | ||
Theorem | cnfrrnsmf 45453 | 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 45454* | The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π΄ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (SMblFnβπ΅)) | ||
Theorem | bormflebmf 45455 | 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 45456* | 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 45457* | 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 45458* | 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 45459* | 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 45460* | 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 45461* | 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 45462* | 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 25127). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = dom vol & β’ (π β π β β) & β’ (π β Β¬ π β π) & β’ πΉ = (π₯ β π β¦ 0) β β’ (π β (πΉ β (SMblFnβπ) β§ Β¬ πΉ β MblFn)) | ||
Theorem | issmfgtd 45463* | 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 45464* | 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 45465* | 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 45466* | 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 45467* | 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 45468* | 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 45469* | 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 45470* | 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 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-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 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-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 45473* | 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 45474* | 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 45475* | 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 45476* | 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 45477* | 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 45478* | 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 45479* | 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 45480* | 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 45481 | 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 45482* | 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 45483* | 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 45484* | 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 45485 | 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 45486* | 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 45487* | 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 45488* | 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 π΄)) | ||
Theorem | smfpimioo 45489 | 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βπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (π΄(,)π΅)) β (π βΎt π·)) | ||
Theorem | smfresal 45490* | Given a sigma-measurable function, the subsets of β whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ π = {π β π« β β£ (β‘πΉ β π) β (π βΎt π·)} β β’ (π β π β SAlg) | ||
Theorem | smfrec 45491* | The reciprocal of a sigma-measurable functions is sigma-measurable. First part of Proposition 121E (e) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ πΆ = {π₯ β π΄ β£ π΅ β 0} β β’ (π β (π₯ β πΆ β¦ (1 / π΅)) β (SMblFnβπ)) | ||
Theorem | smfres 45492 | The restriction of sigma-measurable function is sigma-measurable. Proposition 121E (h) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ (π β π΄ β π) β β’ (π β (πΉ βΎ π΄) β (SMblFnβπ)) | ||
Theorem | smfmullem1 45493 | The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) < π΄) & β’ π = ((π΄ β (π Β· π)) / (1 + ((absβπ) + (absβπ)))) & β’ π = if(1 β€ π, 1, π) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ (π β π» β (π(,)π )) & β’ (π β πΌ β (π(,)π)) β β’ (π β (π» Β· πΌ) < π΄) | ||
Theorem | smfmullem2 45494* | The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ πΎ = {π β (β βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π΄} & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) < π΄) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ π = ((π΄ β (π Β· π)) / (1 + ((absβπ) + (absβπ)))) & β’ π = if(1 β€ π, 1, π) β β’ (π β βπ β πΎ (π β ((πβ0)(,)(πβ1)) β§ π β ((πβ2)(,)(πβ3)))) | ||
Theorem | smfmullem3 45495* | The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β β) & β’ πΎ = {π β (β βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π } & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) < π ) & β’ π = ((π β (π Β· π)) / (1 + ((absβπ) + (absβπ)))) & β’ π = if(1 β€ π, 1, π) β β’ (π β βπ β πΎ (π β ((πβ0)(,)(πβ1)) β§ π β ((πβ2)(,)(πβ3)))) | ||
Theorem | smfmullem4 45496* | The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) & β’ (π β π β β) & β’ πΎ = {π β (β βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π } & β’ πΈ = (π β πΎ β¦ {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) β β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π } β (π βΎt (π΄ β© πΆ))) | ||
Theorem | smfmul 45497* | The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) β β’ (π β (π₯ β (π΄ β© πΆ) β¦ (π΅ Β· π·)) β (SMblFnβπ)) | ||
Theorem | smfmulc1 45498* | A sigma-measurable function multiplied by a constant is sigma-measurable. Proposition 121E (c) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β (SMblFnβπ)) | ||
Theorem | smfdiv 45499* | The fraction of two sigma-measurable functions is measurable. Proposition 121E (e) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β π) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) & β’ πΈ = {π₯ β πΆ β£ π· β 0} β β’ (π β (π₯ β (π΄ β© πΈ) β¦ (π΅ / π·)) β (SMblFnβπ)) | ||
Theorem | smfpimbor1lem1 45500* | Every open set belongs to π. This is the second step in the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ π½ = (topGenβran (,)) & β’ (π β πΊ β π½) & β’ π = {π β π« β β£ (β‘πΉ β π) β (π βΎt π·)} β β’ (π β πΊ β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |