Home | Metamath
Proof Explorer Theorem List (p. 323 of 468) | < 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: | Metamath Proof Explorer
(1-29412) |
Hilbert Space Explorer
(29413-30935) |
Users' Mathboxes
(30936-46791) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ofceq 32201 | Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝑅 = 𝑆 → ∘f/c 𝑅 = ∘f/c 𝑆) | ||
Theorem | ofcfval 32202* | Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofcval 32203 | Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f/c 𝑅𝐶)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofcfn 32204 | The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) Fn 𝐴) | ||
Theorem | ofcfeqd2 32205* | Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝐶) = (𝑦𝑃𝐶)) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f/c 𝑃𝐶)) | ||
Theorem | ofcfval3 32206* | General value of (𝐹 ∘f/c 𝑅𝐶) with no assumptions on functionality of 𝐹. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ dom 𝐹 ↦ ((𝐹‘𝑥)𝑅𝐶))) | ||
Theorem | ofcf 32207* | The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶):𝐴⟶𝑈) | ||
Theorem | ofcfval2 32208* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofcfval4 32209* | The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = ((𝑥 ∈ 𝐵 ↦ (𝑥𝑅𝐶)) ∘ 𝐹)) | ||
Theorem | ofcc 32210 | Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f/c 𝑅𝐶) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | ofcof 32211 | Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐶) = (𝐹 ∘f 𝑅(𝐴 × {𝐶}))) | ||
Syntax | csiga 32212 | Extend class notation to include the function giving the sigma-algebras on a given base set. |
class sigAlgebra | ||
Definition | df-siga 32213* | Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using 𝑆 and 𝑂 as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016.) |
⊢ sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))}) | ||
Theorem | sigaex 32214* | Lemma for issiga 32216 and isrnsiga 32217. The class of sigma-algebras with base set 𝑜 is a set. Note: a more generic version with (𝑂 ∈ V → ...) could be useful for sigaval 32215. (Contributed by Thierry Arnoux, 24-Oct-2016.) |
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))} ∈ V | ||
Theorem | sigaval 32215* | The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.) |
⊢ (𝑂 ∈ V → (sigAlgebra‘𝑂) = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))}) | ||
Theorem | issiga 32216* | An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))) | ||
Theorem | isrnsiga 32217* | The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (Proof shortened by Thierry Arnoux, 23-Oct-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))) | ||
Theorem | 0elsiga 32218 | A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆) | ||
Theorem | baselsiga 32219 | A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝐴 ∈ 𝑆) | ||
Theorem | sigasspw 32220 | A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝑆 ⊆ 𝒫 𝐴) | ||
Theorem | sigaclcu 32221 | A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclcuni 32222* | A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | sigaclfu 32223 | A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin) → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclcu2 32224* | A sigma-algebra is closed under countable union - indexing on ℕ (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ ℕ 𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclfu2 32225* | A sigma-algebra is closed under finite union - indexing on (1..^𝑁). (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) | ||
Theorem | sigaclcu3 32226* | A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆) | ||
Theorem | issgon 32227 | Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016.) (Revised by Thierry Arnoux, 23-Oct-2016.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆)) | ||
Theorem | sgon 32228 | A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) | ||
Theorem | elsigass 32229 | An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → 𝐴 ⊆ ∪ 𝑆) | ||
Theorem | elrnsiga 32230 | Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra) | ||
Theorem | isrnsigau 32231* | The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆)))) | ||
Theorem | unielsiga 32232 | A sigma-algebra contains its universe set. (Contributed by Thierry Arnoux, 13-Feb-2017.) (Shortened by Thierry Arnoux, 6-Jun-2017.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | dmvlsiga 32233 | Lebesgue-measurable subsets of ℝ form a sigma-algebra. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
⊢ dom vol ∈ (sigAlgebra‘ℝ) | ||
Theorem | pwsiga 32234 | Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂)) | ||
Theorem | prsiga 32235 | The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂)) | ||
Theorem | sigaclci 32236 | A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆) | ||
Theorem | difelsiga 32237 | A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆) | ||
Theorem | unelsiga 32238 | A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | inelsiga 32239 | A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | sigainb 32240 | Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ 𝒫 𝐴) ∈ (sigAlgebra‘𝐴)) | ||
Theorem | insiga 32241 | The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂)) | ||
Syntax | csigagen 32242 | Extend class notation to include the sigma-algebra generator. |
class sigaGen | ||
Definition | df-sigagen 32243* | Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}) | ||
Theorem | sigagenval 32244* | Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) = ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠}) | ||
Theorem | sigagensiga 32245 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) ∈ (sigAlgebra‘∪ 𝐴)) | ||
Theorem | sgsiga 32246 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (sigaGen‘𝐴) ∈ ∪ ran sigAlgebra) | ||
Theorem | unisg 32247 | The sigma-algebra generated by a collection 𝐴 is a sigma-algebra on ∪ 𝐴. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → ∪ (sigaGen‘𝐴) = ∪ 𝐴) | ||
Theorem | dmsigagen 32248 | A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ dom sigaGen = V | ||
Theorem | sssigagen 32249 | A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (sigaGen‘𝐴)) | ||
Theorem | sssigagen2 32250 | A subset of the generating set is also a subset of the generated sigma-algebra. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ (sigaGen‘𝐴)) | ||
Theorem | elsigagen 32251 | Any element of a set is also an element of the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 27-Mar-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ (sigaGen‘𝐴)) | ||
Theorem | elsigagen2 32252 | Any countable union of elements of a set is also in the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω) → ∪ 𝐵 ∈ (sigaGen‘𝐴)) | ||
Theorem | sigagenss 32253 | The generated sigma-algebra is a subset of all sigma-algebras containing the generating set, i.e. the generated sigma-algebra is the smallest sigma-algebra containing the generating set, here 𝐴. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ ((𝑆 ∈ (sigAlgebra‘∪ 𝐴) ∧ 𝐴 ⊆ 𝑆) → (sigaGen‘𝐴) ⊆ 𝑆) | ||
Theorem | sigagenss2 32254 | Sufficient condition for inclusion of sigma-algebras. This is used to prove equality of sigma-algebras. (Contributed by Thierry Arnoux, 10-Oct-2017.) |
⊢ ((∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ (sigaGen‘𝐵) ∧ 𝐵 ∈ 𝑉) → (sigaGen‘𝐴) ⊆ (sigaGen‘𝐵)) | ||
Theorem | sigagenid 32255 | The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (sigaGen‘𝑆) = 𝑆) | ||
Because they are not widely used outside of measure theory, we do not introduce specific definitions for lambda- and pi-systems. Instead, we define 𝑃 and 𝐿 respectively as the classes of pi- and lambda-systems in 𝑂 throughout this section. | ||
Theorem | ispisys 32256* | The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑆) ⊆ 𝑆)) | ||
Theorem | ispisys2 32257* | The property of being a pi-system, expanded version. Pi-systems are closed under finite intersections. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀𝑥 ∈ ((𝒫 𝑆 ∩ Fin) ∖ {∅})∩ 𝑥 ∈ 𝑆)) | ||
Theorem | inelpisys 32258* | Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ ((𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | sigapisys 32259* | All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ (sigAlgebra‘𝑂) ⊆ 𝑃 | ||
Theorem | isldsys 32260* | The property of being a lambda-system or Dynkin system. Lambda-systems contain the empty set, are closed under complement, and closed under countable disjoint union. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆)))) | ||
Theorem | pwldsys 32261* | The power set of the universe set 𝑂 is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿) | ||
Theorem | unelldsys 32262* | Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑆 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | sigaldsys 32263* | All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (sigAlgebra‘𝑂) ⊆ 𝐿 | ||
Theorem | ldsysgenld 32264* | The intersection of all lambda-systems containing a given collection of sets 𝐴, which is called the lambda-system generated by 𝐴, is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑂) ⇒ ⊢ (𝜑 → ∩ {𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡} ∈ 𝐿) | ||
Theorem | sigapildsyslem 32265* | Lemma for sigapildsys 32266. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑡 ∈ (𝑃 ∩ 𝐿)) & ⊢ (𝜑 → 𝐴 ∈ 𝑡) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡) ⇒ ⊢ (𝜑 → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) ∈ 𝑡) | ||
Theorem | sigapildsys 32266* | Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (sigAlgebra‘𝑂) = (𝑃 ∩ 𝐿) | ||
Theorem | ldgenpisyslem1 32267* | Lemma for ldgenpisys 32270. (Contributed by Thierry Arnoux, 29-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) ⇒ ⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿) | ||
Theorem | ldgenpisyslem2 32268* | Lemma for ldgenpisys 32270. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝑇 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ⇒ ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | ||
Theorem | ldgenpisyslem3 32269* | Lemma for ldgenpisys 32270. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) ⇒ ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | ||
Theorem | ldgenpisys 32270* | The lambda system 𝐸 generated by a pi-system 𝑇 is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑃) | ||
Theorem | dynkin 32271* | Dynkin's lambda-pi theorem: if a lambda-system contains a pi-system, it also contains the sigma-algebra generated by that pi-system. (Contributed by Thierry Arnoux, 16-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝐿) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ∩ {𝑢 ∈ (sigAlgebra‘𝑂) ∣ 𝑇 ⊆ 𝑢} ⊆ 𝑆) | ||
Theorem | isros 32272* | The property of being a rings of sets, i.e. containing the empty set, and closed under finite union and set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ (𝑆 ∈ 𝑄 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ((𝑢 ∪ 𝑣) ∈ 𝑆 ∧ (𝑢 ∖ 𝑣) ∈ 𝑆))) | ||
Theorem | rossspw 32273* | A ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ (𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂) | ||
Theorem | 0elros 32274* | A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆) | ||
Theorem | unelros 32275* | A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | difelros 32276* | A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆) | ||
Theorem | inelros 32277* | A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | fiunelros 32278* | A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} & ⊢ (𝜑 → 𝑆 ∈ 𝑄) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆) | ||
Theorem | issros 32279* | The property of being a semirings of sets, i.e., collections of sets containing the empty set, closed under finite intersection, and where complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑁 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))) | ||
Theorem | srossspw 32280* | A semiring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑁 → 𝑆 ⊆ 𝒫 𝑂) | ||
Theorem | 0elsros 32281* | A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑁 → ∅ ∈ 𝑆) | ||
Theorem | inelsros 32282* | A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | diffiunisros 32283* | In semiring of sets, complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧)) | ||
Theorem | rossros 32284* | Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} & ⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁) | ||
Syntax | cbrsiga 32285 | The Borel Algebra on real numbers, usually a gothic B |
class 𝔅ℝ | ||
Definition | df-brsiga 32286 | A Borel Algebra is defined as a sigma-algebra generated by a topology. 'The' Borel sigma-algebra here refers to the sigma-algebra generated by the topology of open intervals on real numbers. The Borel algebra of a given topology 𝐽 is the sigma-algebra generated by 𝐽, (sigaGen‘𝐽), so there is no need to introduce a special constant function for Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ 𝔅ℝ = (sigaGen‘(topGen‘ran (,))) | ||
Theorem | brsiga 32287 | The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ 𝔅ℝ ∈ (sigaGen “ Top) | ||
Theorem | brsigarn 32288 | The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ 𝔅ℝ ∈ (sigAlgebra‘ℝ) | ||
Theorem | brsigasspwrn 32289 | The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ 𝔅ℝ ⊆ 𝒫 ℝ | ||
Theorem | unibrsiga 32290 | The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ ∪ 𝔅ℝ = ℝ | ||
Theorem | cldssbrsiga 32291 | A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.) |
⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽)) | ||
Syntax | csx 32292 | Extend class notation with the product sigma-algebra operation. |
class ×s | ||
Definition | df-sx 32293* | Define the product sigma-algebra operation, analogous to df-tx 22793. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ×s = (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦)))) | ||
Theorem | sxval 32294* | Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ 𝐴 = ran (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑇 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ×s 𝑇) = (sigaGen‘𝐴)) | ||
Theorem | sxsiga 32295 | A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra) | ||
Theorem | sxsigon 32296 | A product sigma-algebra is a sigma-algebra on the product of the bases. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ (sigAlgebra‘(∪ 𝑆 × ∪ 𝑇))) | ||
Theorem | sxuni 32297 | The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) | ||
Theorem | elsx 32298 | The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.) |
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐴 × 𝐵) ∈ (𝑆 ×s 𝑇)) | ||
Syntax | cmeas 32299 | Extend class notation to include the class of measures. |
class measures | ||
Definition | df-meas 32300* | Define a measure as a nonnegative countably additive function over a sigma-algebra onto (0[,]+∞). (Contributed by Thierry Arnoux, 10-Sep-2016.) |
⊢ measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |