Home | Metamath
Proof Explorer Theorem List (p. 410 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vonn0ioo 40901* | 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.) |
voln | ||
Theorem | vonn0icc 40902* | 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.) |
voln | ||
Theorem | ctvonmbl 40903 | 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.) |
voln | ||
Theorem | vonn0ioo2 40904* | 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.) |
voln | ||
Theorem | vonsn 40905 | 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.) |
voln | ||
Theorem | vonn0icc2 40906* | 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.) |
voln | ||
Theorem | vonct 40907 | 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.) |
voln | ||
Theorem | vitali2 40908 | There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 9317). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
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 w.r.t. df-mbf 23388 are also sigma-measurable, but the definition in this section considers as measurable functions, some that are not measurable w.r.t. df-mbf 23388 (see mbfpsssmf 40991 and smfmbfcex 40968). | ||
Syntax | csmblfn 40909 | Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras. |
SMblFn | ||
Definition | df-smblfn 40910* | 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 ↾t | ||
Theorem | pimltmnf2 40911* | 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.) |
Theorem | preimagelt 40912* | The preimage of a right-open, unbounded below interval, is the complement of a left-close, unbounded above interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | preimalegt 40913* | The preimage of a left-open, unbounded above interval, is the complement of a right-close, unbounded below interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | pimconstlt0 40914* | Given a constant function, its preimage with respect to an unbounded below, open interval, with upper bound smaller 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 40915* | 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 | pimltpnf 40916* | 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.) |
Theorem | pimgtpnf2 40917* | 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.) |
Theorem | salpreimagelt 40918* | If all the preimages of left-close, 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 40919 | The preimage of an unbounded below, open interval, with positive upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | salpreimalegt 40920* | 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 40921* | 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 40922* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | pimltpnf2 40923* | 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.) |
Theorem | pimgtmnf2 40924* | 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 40925* | Given a non-increasing 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.) |
Theorem | pimincfltioc 40926* | Given a non decreasing 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.) |
Theorem | pimdecfgtioo 40927* | Given a non decreasing 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.) |
Theorem | pimincfltioo 40928* | Given a non decreasing 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.) |
Theorem | preimaioomnf 40929* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | preimageiingt 40930* | 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.) |
Theorem | preimaleiinlt 40931* | 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.) |
Theorem | pimgtmnf 40932* | 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 | pimrecltneg 40933 | The preimage of an unbounded below, open interval, with negative upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | salpreimagtge 40934* | 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 40935* | 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 40936* | 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 SMblFn ↾t | ||
Theorem | issmf 40937* | 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 SMblFn ↾t | ||
Theorem | salpreimalelt 40938* | If all the preimages of right-close, 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 40939* | 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 40940* | 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 | smff 40941 | A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SAlg SMblFn | ||
Theorem | smfdmss 40942 | 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 | ||
Theorem | issmff 40943* | 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 SMblFn ↾t | ||
Theorem | issmfd 40944* | 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 40945* | 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 | issmfdf 40946* | 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 40947 | The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | mbfresmf 40948 | 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 SMblFn | ||
Theorem | cnfsmf 40949 | 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.) |
↾t SalGen SMblFn | ||
Theorem | incsmflem 40950* | A non decreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGen | ||
Theorem | incsmf 40951* | A real-valued, non-decreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGen SMblFn | ||
Theorem | smfsssmf 40952 | 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 40953* | 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 ↾t SMblFn | ||
Theorem | issmfle 40954* | 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 SMblFn ↾t | ||
Theorem | smfpimltmpt 40955* | 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 40956* | 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 | issmfdmpt 40957* | 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 40958* | 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 40959* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | cnfrrnsmf 40960 | 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.) |
ℝ^ ↾t SalGen SMblFn | ||
Theorem | smfid 40961* | The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGen SMblFn | ||
Theorem | bormflebmf 40962 | A Borel measurable function is Lebesgue measurable. Proposition 121D (a) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGenℝ^ voln SMblFn SMblFn | ||
Theorem | smfpreimale 40963* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an 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 ↾t | ||
Theorem | issmfgtlem 40964* | 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 ↾t SMblFn | ||
Theorem | issmfgt 40965* | 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 SMblFn ↾t | ||
Theorem | issmfled 40966* | 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 | smfpimltxrmpt 40967* | 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 | smfmbfcex 40968* | 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 23388). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SMblFn MblFn | ||
Theorem | issmfgtd 40969* | 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 40970* | 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 | smfaddlem1 40971* | 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 40972* | 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 40973* | 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 40974* | A non-increasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGen | ||
Theorem | decsmf 40975* | A real-valued, non-increasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGen SMblFn | ||
Theorem | smfpreimagtf 40976* | 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 | issmfgelem 40977* | 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 ↾t SMblFn | ||
Theorem | issmfge 40978* | 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 SMblFn ↾t | ||
Theorem | smflimlem1 40979* | 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 ↾t | ||
Theorem | smflimlem2 40980* | 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 | ||
Theorem | smflimlem3 40981* | 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 | ||
Theorem | smflimlem4 40982* | 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 | ||
Theorem | smflimlem5 40983* | 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 ↾t | ||
Theorem | smflimlem6 40984* | 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 ↾t | ||
Theorem | smflim 40985* | 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 SMblFn | ||
Theorem | nsssmfmbflem 40986* | 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.) |
SMblFn MblFn | ||
Theorem | nsssmfmbf 40987 | 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.) |
SMblFn MblFn | ||
Theorem | smfpimgtxr 40988* | 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 | smfpimgtmpt 40989* | 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 40990* | 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 ↾t | ||
Theorem | mbfpsssmf 40991 | 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.) |
MblFn SMblFn | ||
Theorem | smfpimgtxrmpt 40992* | 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 | smfpimioompt 40993* | 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 40994 | 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 | smfresal 40995* | 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 ↾t SAlg | ||
Theorem | smfrec 40996* | 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 SMblFn | ||
Theorem | smfres 40997 | 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 40998 | 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.) |
Theorem | smfmullem2 40999* | 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.) |
Theorem | smfmullem3 41000* | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |