| Metamath
Proof Explorer Theorem List (p. 468 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | snvonmbl 46701 | A n-dimensional singleton is Lebesgue measurable. This is the first statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → {𝐴} ∈ dom (voln‘𝑋)) | ||
| Theorem | vonn0ioo 46702* | 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 46703* | 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 46704 | 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 46705* | 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 46706 | 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 46707* | 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 46708 | 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 46709 | There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 10535). (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 25654 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 25654 (see mbfpsssmf 46798 and smfmbfcex 46775). | ||
| Syntax | csmblfn 46710 | Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras. |
| class SMblFn | ||
| Definition | df-smblfn 46711* | 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 46712 | 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 46713* | 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 46714* | 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 46715* | 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 46716* | 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 46717* | 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 46718 | 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 46719* | 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 46720 | 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 46721* | 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 46722* | 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 46723 | 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 46724* | 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 46725* | 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 46726* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (◡𝐹 “ (-∞[,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵}) | ||
| Theorem | pimltpnf2f 46727 | 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 46728* | 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 46729* | 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 46730* | 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 46731* | 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 46732* | 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 46733* | 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 46734* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵}) | ||
| Theorem | preimageiingt 46735* | 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 46736* | 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 46737 | 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 46738* | 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 46739 | 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 46740* | 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 46741* | 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 46742* | 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 46743* | 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 46744* | 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 46745* | 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 46746* | 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 46747 | 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 46748 | 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 46749* | 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 46750* | 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 46751* | 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 46752* | 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 46753 | The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (SMblFn‘𝑆)) | ||
| Theorem | mbfresmf 46754 | 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 46755 | 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 46756* | 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 46757* | 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 46758 | 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 46759* | 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 46760* | 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 46761* | 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 46762* | 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 46763* | 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 46764* | 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 46765* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | ||
| Theorem | cnfrrnsmf 46766 | 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 46767* | The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (SMblFn‘𝐵)) | ||
| Theorem | bormflebmf 46768 | 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 46769* | 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 46770* | 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 46771* | 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 46772* | 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 46773* | 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 46774* | 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 46775* | 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 25654). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝑆 = dom vol & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 0) ⇒ ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ∧ ¬ 𝐹 ∈ MblFn)) | ||
| Theorem | issmfgtd 46776* | 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 46777* | 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 46778* | 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 46779* | 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 46780* | 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 46781* | 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 46782* | 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 46783* | 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 46784* | 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 46785* | 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 46786* | 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 46787* | 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 46788* | 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 46789* | 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 46790* | 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 46791* | 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 46792* | 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 46793* | 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 46794 | 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 46795* | 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 46796* | 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 46797* | 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 46798 | 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 46799* | 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 46800* | 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 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |