![]() |
Metamath
Proof Explorer Theorem List (p. 427 of 445) | < 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-28382) |
![]() (28383-29905) |
![]() (29906-44433) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | issmfgtd 42601* | 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 42602* | 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 42603* | 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 42604* | 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 42605* | 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 42606* | 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 42607* | 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 42608* | 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 42609* | 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 42610* | 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 42611* | 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 42612* | 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 42613* | 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 42614* | 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 42615* | 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 42616* | 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 42617* | 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 42618* | 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 42619 | 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 42620* | 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 | smfpimgtmpt 42621* | 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 42622* | 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 42623 | 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 | smfpimgtxrmpt 42624* | 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 42625* | 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 42626 | 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 42627* | 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 42628* | 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 42629 | 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 42630 | 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 42631* | 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.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ 𝐾 = {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴} & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝑉 ∈ ℝ) & ⊢ (𝜑 → (𝑈 · 𝑉) < 𝐴) & ⊢ (𝜑 → 𝑃 ∈ ℚ) & ⊢ (𝜑 → 𝑅 ∈ ℚ) & ⊢ (𝜑 → 𝑆 ∈ ℚ) & ⊢ (𝜑 → 𝑍 ∈ ℚ) & ⊢ (𝜑 → 𝑃 ∈ ((𝑈 − 𝑌)(,)𝑈)) & ⊢ (𝜑 → 𝑅 ∈ (𝑈(,)(𝑈 + 𝑌))) & ⊢ (𝜑 → 𝑆 ∈ ((𝑉 − 𝑌)(,)𝑉)) & ⊢ (𝜑 → 𝑍 ∈ (𝑉(,)(𝑉 + 𝑌))) & ⊢ 𝑋 = ((𝐴 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉)))) & ⊢ 𝑌 = if(1 ≤ 𝑋, 1, 𝑋) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐾 (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3)))) | ||
Theorem | smfmullem3 42632* | 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.) |
⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ 𝐾 = {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝑉 ∈ ℝ) & ⊢ (𝜑 → (𝑈 · 𝑉) < 𝑅) & ⊢ 𝑋 = ((𝑅 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉)))) & ⊢ 𝑌 = if(1 ≤ 𝑋, 1, 𝑋) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐾 (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3)))) | ||
Theorem | smfmullem4 42633* | 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‘𝑆)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ 𝐾 = {𝑞 ∈ (ℚ ↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} & ⊢ 𝐸 = (𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) ⇒ ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) | ||
Theorem | smfmul 42634* | 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 42635* | 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 42636* | 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 42637* | 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 42638* | 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 42639 | 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 42640* | 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 42641 | 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 42642* | The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (SMblFn‘𝑆)) | ||
Theorem | smffmpt 42643* | 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 42644* | 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 42617 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) | ||
Theorem | smfpimcclem 42645* | Lemma for smfpimcc 42646 given the choice function 𝐶. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ 𝑍 ∈ 𝑉 & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))})) → (𝐶‘𝑦) ∈ 𝑦) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝐶‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))})) ⇒ ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) | ||
Theorem | smfpimcc 42646* | 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 42647* | 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 42648* | 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 42649* | 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 42650* | 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 42651* | 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 42652* | 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 42653* | 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 42654* | 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 42655* | 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 42656* | 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 42657* | 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 42658* | If 𝐻 converges, the lim sup of 𝐹 is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ))) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) ⇒ ⊢ (𝜑 → dom (𝐻‘𝐾) ⊆ dom (𝐹‘𝐾)) | ||
Theorem | smflimsuplem2 42659* | 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 42660* | 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 42661* | 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 42662* | 𝐻 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 42663* | 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 42664* | 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 42665* | 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 42666* | 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 42667* | 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 42668* | 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 42669* | 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 42670* | 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 | sigarval 42671* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = (ℑ‘((∗‘𝐴) · 𝐵))) | ||
Theorem | sigarim 42672* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) ∈ ℝ) | ||
Theorem | sigarac 42673* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴)) | ||
Theorem | sigaraf 42674* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) + (𝐶𝐺𝐵))) | ||
Theorem | sigarmf 42675* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) − (𝐶𝐺𝐵))) | ||
Theorem | sigaras 42676* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 + 𝐶)) = ((𝐴𝐺𝐵) + (𝐴𝐺𝐶))) | ||
Theorem | sigarms 42677* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶))) | ||
Theorem | sigarls 42678* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ) → (𝐴𝐺(𝐵 · 𝐶)) = ((𝐴𝐺𝐵) · 𝐶)) | ||
Theorem | sigarid 42679* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ (𝐴 ∈ ℂ → (𝐴𝐺𝐴) = 0) | ||
Theorem | sigarexp 42680* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = (((𝐴𝐺𝐵) − (𝐴𝐺𝐶)) − (𝐶𝐺𝐵))) | ||
Theorem | sigarperm 42681* | Signed area (𝐴 − 𝐶)𝐺(𝐵 − 𝐶) acts as a double area of a triangle 𝐴𝐵𝐶. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴))) | ||
Theorem | sigardiv 42682* | If signed area between vectors 𝐵 − 𝐴 and 𝐶 − 𝐴 is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → ¬ 𝐶 = 𝐴) & ⊢ (𝜑 → ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)) = 0) ⇒ ⊢ (𝜑 → ((𝐵 − 𝐴) / (𝐶 − 𝐴)) ∈ ℝ) | ||
Theorem | sigarimcd 42683* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ⇒ ⊢ (𝜑 → (𝐴𝐺𝐵) ∈ ℂ) | ||
Theorem | sigariz 42684* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) & ⊢ (𝜑 → (𝐴𝐺𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵𝐺𝐴) = 0) | ||
Theorem | sigarcol 42685* | Given three points 𝐴, 𝐵 and 𝐶 such that ¬ 𝐴 = 𝐵, the point 𝐶 lies on the line going through 𝐴 and 𝐵 iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = 0 ↔ ∃𝑡 ∈ ℝ 𝐶 = (𝐵 + (𝑡 · (𝐴 − 𝐵))))) | ||
Theorem | sharhght 42686* | Let 𝐴𝐵𝐶 be a triangle, and let 𝐷 lie on the line 𝐴𝐵. Then (doubled) areas of triangles 𝐴𝐷𝐶 and 𝐶𝐷𝐵 relate as lengths of corresponding bases 𝐴𝐷 and 𝐷𝐵. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)) ⇒ ⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷))) | ||
Theorem | sigaradd 42687* | Subtracting (double) area of 𝐴𝐷𝐶 from 𝐴𝐵𝐶 yields the (double) area of 𝐷𝐵𝐶. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)) ⇒ ⊢ (𝜑 → (((𝐵 − 𝐶)𝐺(𝐴 − 𝐶)) − ((𝐷 − 𝐶)𝐺(𝐴 − 𝐶))) = ((𝐵 − 𝐶)𝐺(𝐷 − 𝐶))) | ||
Theorem | cevathlem1 42688 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) & ⊢ (𝜑 → (𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0)) & ⊢ (𝜑 → ((𝐴 · 𝐵) = (𝐶 · 𝐷) ∧ (𝐸 · 𝐹) = (𝐴 · 𝐺) ∧ (𝐶 · 𝐻) = (𝐸 · 𝐾))) ⇒ ⊢ (𝜑 → ((𝐵 · 𝐹) · 𝐻) = ((𝐷 · 𝐺) · 𝐾)) | ||
Theorem | cevathlem2 42689* | Ceva's theorem second lemma. Relate (doubled) areas of triangles 𝐶𝐴𝑂 and 𝐴𝐵𝑂 with of segments 𝐵𝐷 and 𝐷𝐶. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → 𝑂 ∈ ℂ) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0)) ⇒ ⊢ (𝜑 → (((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) · (𝐵 − 𝐷)) = (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) · (𝐷 − 𝐶))) | ||
Theorem | cevath 42690* |
Ceva's theorem. Let 𝐴𝐵𝐶 be a triangle and let points 𝐹,
𝐷 and 𝐸 lie on sides 𝐴𝐵, 𝐵𝐶, 𝐶𝐴
correspondingly. Suppose that cevians 𝐴𝐷, 𝐵𝐸 and 𝐶𝐹
intersect at one point 𝑂. Then triangle's sides are
partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 42689 three times and then using cevathlem1 42688 to multiply obtained identities and prove the theorem. In the theorem statement we are using function 𝐺 as a collinearity indicator. For justification of that use, see sigarcol 42685. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦))) & ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) & ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → 𝑂 ∈ ℂ) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0)) & ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0)) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐹) · (𝐶 − 𝐸)) · (𝐵 − 𝐷)) = (((𝐹 − 𝐵) · (𝐸 − 𝐴)) · (𝐷 − 𝐶))) | ||
Theorem | hirstL-ax3 42691 | The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜑)) | ||
Theorem | ax3h 42692 | Recover ax-3 8 from hirstL-ax3 42691. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | aibandbiaiffaiffb 42693 | A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | aibandbiaiaiffb 42694 | A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)) | ||
Theorem | notatnand 42695 | Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) | ||
Theorem | aistia 42696 | Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
⊢ (𝜑 ↔ ⊤) ⇒ ⊢ 𝜑 | ||
Theorem | aisfina 42697 | Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
⊢ (𝜑 ↔ ⊥) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | bothtbothsame 42698 | Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ (𝜑 ↔ ⊤) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | bothfbothsame 42699 | Given both a, b are equivalent to ⊥, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
⊢ (𝜑 ↔ ⊥) & ⊢ (𝜓 ↔ ⊥) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | aiffbbtat 42700 | Given a is equivalent to b, b is equivalent to ⊤ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ↔ ⊤) ⇒ ⊢ (𝜑 ↔ ⊤) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |