![]() |
Metamath
Proof Explorer Theorem List (p. 468 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfpimltmpt 46701* | 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 46702* | 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 46703* | 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 46704* | 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 46705* | The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | ||
Theorem | cnfrrnsmf 46706 | 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 46707* | The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (SMblFn‘𝐵)) | ||
Theorem | bormflebmf 46708 | 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 46709* | 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 46710* | 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 46711* | 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 46712* | 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 46713* | 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 46714* | 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 46715* | 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 25667). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑆 = dom vol & ⊢ (𝜑 → 𝑋 ⊆ ℝ) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 0) ⇒ ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ∧ ¬ 𝐹 ∈ MblFn)) | ||
Theorem | issmfgtd 46716* | 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 46717* | 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 46718* | 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 46719* | 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 46720* | 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 46721* | 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 46722* | 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 46723* | 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 46724* | 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 46725* | 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 46726* | 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 46727* | 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 46728* | 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 46729* | 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 46730* | 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 46731* | 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 46732* | 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 46733* | 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 46734 | 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 46735* | 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 46736* | 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 46737* | 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 46738 | 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 46739* | 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 46740* | 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 46741* | 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 46742 | 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 46743* | 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 46744* | 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 46745 | 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 46746 | 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 46747* | 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 46748* | 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 46749* | 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 46750* | 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 46751* | 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 46752* | 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 46753* | 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 𝐷)} ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑇) | ||
Theorem | smfpimbor1lem2 46754* | Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = dom 𝐹 & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ 𝑃 = (◡𝐹 “ 𝐸) & ⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝑆 ↾t 𝐷)) | ||
Theorem | smfpimbor1 46755 | Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = dom 𝐹 & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ 𝑃 = (◡𝐹 “ 𝐸) ⇒ ⊢ (𝜑 → 𝑃 ∈ (𝑆 ↾t 𝐷)) | ||
Theorem | smf2id 46756* | Twice the identity function is Borel sigma-measurable (just an example, to test previous general theorems). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (2 · 𝑥)) ∈ (SMblFn‘𝐵)) | ||
Theorem | smfco 46757 | The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐻 ∈ (SMblFn‘𝐵)) ⇒ ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ (SMblFn‘𝑆)) | ||
Theorem | smfneg 46758* | The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (SMblFn‘𝑆)) | ||
Theorem | smffmptf 46759 | A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) | ||
Theorem | smffmpt 46760* | A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) | ||
Theorem | smflim2 46761* | The limit of a sequence 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 ). TODO: this has fewer distinct variable conditions than smflim 46732 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfpimcclem 46762* | Lemma for smfpimcc 46763 given the choice function 𝐶. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ 𝑍 ∈ 𝑉 & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))})) → (𝐶‘𝑦) ∈ 𝑦) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝐶‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))})) ⇒ ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) | ||
Theorem | smfpimcc 46763* | Given a countable set of sigma-measurable functions, and a Borel set 𝐴 there exists a choice function ℎ that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of 𝐴. This is a generalization of the observation at the beginning of the proof of Proposition 121F of [Fremlin1] p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) | ||
Theorem | issmfle2d 46764* | A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑎𝜑 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,]𝑎)) ∈ (𝑆 ↾t 𝐷)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) | ||
Theorem | smflimmpt 46765* | The limit of a sequence 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 ). 𝐴 can contain 𝑚 as a free variable, in other words it can be thought as an indexed collection 𝐴(𝑚). 𝐵 can be thought as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfsuplem1 46766* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐻:𝑍⟶𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛))) ⇒ ⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷)) | ||
Theorem | smfsuplem2 46767* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷)) | ||
Theorem | smfsuplem3 46768* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfsup 46769* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfsupmpt 46770* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfsupxr 46771* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ*, < ) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ*, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfinflem 46772* | The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfinf 46773* | The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfinfmpt 46774* | The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smflimsuplem1 46775* | If 𝐻 converges, the lim sup of 𝐹 is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) ⇒ ⊢ (𝜑 → dom (𝐻‘𝐾) ⊆ dom (𝐹‘𝐾)) | ||
Theorem | smflimsuplem2 46776* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) & ⊢ (𝜑 → 𝑛 ∈ 𝑍) & ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → 𝑋 ∈ dom (𝐻‘𝑛)) | ||
Theorem | smflimsuplem3 46777* | The limit of the (𝐻‘𝑛) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) ⇒ ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ (ℤ≥‘𝑘)dom (𝐻‘𝑛) ∣ (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)))) ∈ (SMblFn‘𝑆)) | ||
Theorem | smflimsuplem4 46778* | If 𝐻 converges, the lim sup of 𝐹 is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝑥 ∈ ∩ 𝑛 ∈ (ℤ≥‘𝑁)dom (𝐻‘𝑛)) & ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | ||
Theorem | smflimsuplem5 46779* | 𝐻 converges to the superior limit of 𝐹. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) & ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑁)dom (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑋)) ⇝ (lim sup‘(𝑚 ∈ (ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑋)))) | ||
Theorem | smflimsuplem6 46780* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) & ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑁)dom (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑋)) ∈ dom ⇝ ) | ||
Theorem | smflimsuplem7 46781* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} & ⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) ⇒ ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) | ||
Theorem | smflimsuplem8 46782* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smflimsup 46783* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smflimsupmpt 46784* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfliminflem 46785* | The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfliminf 46786* | The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfliminfmpt 46787* | The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | adddmmbl 46788 | If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → dom (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ (𝐶 + 𝐷)) ∈ 𝑆) | ||
Theorem | adddmmbl2 46789 | If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → dom 𝐹 ∈ 𝑆) & ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) & ⊢ 𝐻 = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → dom 𝐻 ∈ 𝑆) | ||
Theorem | muldmmbl 46790 | If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → dom (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ (𝐶 · 𝐷)) ∈ 𝑆) | ||
Theorem | muldmmbl2 46791 | If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → dom 𝐹 ∈ 𝑆) & ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) & ⊢ 𝐻 = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → dom 𝐻 ∈ 𝑆) | ||
Theorem | smfdmmblpimne 46792* | If a measurable function w.r.t. to a sigma-algebra has domain in the sigma-algebra, the set of elements that are not mapped to a given real, is in the sigma-algebra (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶} ⇒ ⊢ (𝜑 → 𝐷 ∈ 𝑆) | ||
Theorem | smfdivdmmbl 46793 | If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator (it is needed only for the function at the denominator). (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ (SMblFn‘𝑆)) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ 𝐷 ≠ 0} ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐸) ∈ 𝑆) | ||
Theorem | smfpimne 46794* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value in the extended reals is in the subspace of sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = dom 𝐹 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≠ 𝐴} ∈ (𝑆 ↾t 𝐷)) | ||
Theorem | smfpimne2 46795* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value is in the subspace sigma-algebra induced by its domain. Notice that 𝐴 is not assumed to be an extended real. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) & ⊢ 𝐷 = dom 𝐹 ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≠ 𝐴} ∈ (𝑆 ↾t 𝐷)) | ||
Theorem | smfdivdmmbl2 46796 | If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator. It is required only for the function at the denominator. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑉) & ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) & ⊢ 𝐷 = {𝑥 ∈ dom 𝐺 ∣ (𝐺‘𝑥) ≠ 0} & ⊢ 𝐻 = (𝑥 ∈ (dom 𝐹 ∩ 𝐷) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → dom 𝐻 ∈ 𝑆) | ||
Theorem | fsupdm 46797* | The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚})) ⇒ ⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) | ||
Theorem | fsupdm2 46798* | The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚})) ⇒ ⊢ (𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚)) | ||
Theorem | smfsupdmmbllem 46799* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚})) & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) | ||
Theorem | smfsupdmmbl 46800* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆) & ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) ⇒ ⊢ (𝜑 → dom 𝐺 ∈ 𝑆) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |