![]() |
Metamath
Proof Explorer Theorem List (p. 296 of 424) | < 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-27159) |
![]() (27160-28684) |
![]() (28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | issiga 29501* | An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))) | ||
Theorem | isrnsigaOLD 29502* | The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))) | ||
Theorem | isrnsiga 29503* | 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 29504 | A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆) | ||
Theorem | baselsiga 29505 | A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝐴 ∈ 𝑆) | ||
Theorem | sigasspw 29506 | A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝑆 ⊆ 𝒫 𝐴) | ||
Theorem | sigaclcu 29507 | A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclcuni 29508* | A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | sigaclfu 29509 | A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin) → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclcu2 29510* | A sigma-algebra is closed under countable union - indexing on ℕ (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ ℕ 𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclfu2 29511* | A sigma-algebra is closed under finite union - indexing on (1..^𝑁). (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) | ||
Theorem | sigaclcu3 29512* | A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆) | ||
Theorem | issgon 29513 | 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 29514 | A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) | ||
Theorem | elsigass 29515 | An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → 𝐴 ⊆ ∪ 𝑆) | ||
Theorem | elrnsiga 29516 | Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra) | ||
Theorem | isrnsigau 29517* | The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆)))) | ||
Theorem | unielsiga 29518 | 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 29519 | 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 29520 | Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂)) | ||
Theorem | prsiga 29521 | The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂)) | ||
Theorem | sigaclci 29522 | A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆) | ||
Theorem | difelsiga 29523 | A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆) | ||
Theorem | unelsiga 29524 | A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | inelsiga 29525 | A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | sigainb 29526 | Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ 𝒫 𝐴) ∈ (sigAlgebra‘𝐴)) | ||
Theorem | insiga 29527 | 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 29528 | Extend class notation to include the sigma-algebra generator. |
class sigaGen | ||
Definition | df-sigagen 29529* | 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 29530* | Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) = ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠}) | ||
Theorem | sigagensiga 29531 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) ∈ (sigAlgebra‘∪ 𝐴)) | ||
Theorem | sgsiga 29532 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (sigaGen‘𝐴) ∈ ∪ ran sigAlgebra) | ||
Theorem | unisg 29533 | The sigma-algebra generated by a collection 𝐴 is a sigma-algebra on ∪ 𝐴. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → ∪ (sigaGen‘𝐴) = ∪ 𝐴) | ||
Theorem | dmsigagen 29534 | A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ dom sigaGen = V | ||
Theorem | sssigagen 29535 | A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (sigaGen‘𝐴)) | ||
Theorem | sssigagen2 29536 | 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 29537 | 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 29538 | 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 29539 | 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 29540 | 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 29541 | 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 don't introduce specific definitions for lambda- and pi-systems. Instead, we are defining 𝑃 and 𝐿 respectively as the classes of pi- and lambda-systems in 𝑂 throughout this section. | ||
Theorem | ispisys 29542* | The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑆) ⊆ 𝑆)) | ||
Theorem | ispisys2 29543* | 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 29544* | Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ ((𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | sigapisys 29545* | All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⇒ ⊢ (sigAlgebra‘𝑂) ⊆ 𝑃 | ||
Theorem | isldsys 29546* | 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 29547* | The power set of the universe set 𝑂 is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿) | ||
Theorem | unelldsys 29548* | Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑆 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | sigaldsys 29549* | All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (sigAlgebra‘𝑂) ⊆ 𝐿 | ||
Theorem | ldsysgenld 29550* | 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 29551* | Lemma for sigapildsys 29552. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑡 ∈ (𝑃 ∩ 𝐿)) & ⊢ (𝜑 → 𝐴 ∈ 𝑡) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡) ⇒ ⊢ (𝜑 → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) ∈ 𝑡) | ||
Theorem | sigapildsys 29552* | Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⇒ ⊢ (sigAlgebra‘𝑂) = (𝑃 ∩ 𝐿) | ||
Theorem | ldgenpisyslem1 29553* | Lemma for ldgenpisys 29556. (Contributed by Thierry Arnoux, 29-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) ⇒ ⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿) | ||
Theorem | ldgenpisyslem2 29554* | Lemma for ldgenpisys 29556. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝑇 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) ⇒ ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | ||
Theorem | ldgenpisyslem3 29555* | Lemma for ldgenpisys 29556. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) ⇒ ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸}) | ||
Theorem | ldgenpisys 29556* | The lambda system 𝐸 generated by a pi-system 𝑇 is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.) |
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} & ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} & ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} & ⊢ (𝜑 → 𝑇 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑃) | ||
Theorem | dynkin 29557* | 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 29558* | 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 29559* | A ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ (𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂) | ||
Theorem | 0elros 29560* | A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆) | ||
Theorem | unelros 29561* | A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | difelros 29562* | A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆) | ||
Theorem | inelros 29563* | A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} ⇒ ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | fiunelros 29564* | A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} & ⊢ (𝜑 → 𝑆 ∈ 𝑄) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆) | ||
Theorem | issros 29565* | The property of being a semi-rings 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 29566* | A semi-ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑁 → 𝑆 ⊆ 𝒫 𝑂) | ||
Theorem | 0elsros 29567* | A semi-ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑁 → ∅ ∈ 𝑆) | ||
Theorem | inelsros 29568* | A semi-ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | diffiunisros 29569* | 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 29570* | Rings of sets are semi-rings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))} & ⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} ⇒ ⊢ (𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁) | ||
Syntax | cbrsiga 29571 | The Borel Algebra on real numbers, usually a gothic B |
class 𝔅ℝ | ||
Definition | df-brsiga 29572 | 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 29573 | The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ 𝔅ℝ ∈ (sigaGen “ Top) | ||
Theorem | brsigarn 29574 | The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ 𝔅ℝ ∈ (sigAlgebra‘ℝ) | ||
Theorem | brsigasspwrn 29575 | The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ 𝔅ℝ ⊆ 𝒫 ℝ | ||
Theorem | unibrsiga 29576 | The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ ∪ 𝔅ℝ = ℝ | ||
Theorem | cldssbrsiga 29577 | A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.) |
⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽)) | ||
Syntax | csx 29578 | Extend class notation with the product sigma-algebra operation. |
class ×s | ||
Definition | df-sx 29579* | Define the product sigma-algebra operation, analogous to df-tx 21175. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ×s = (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦)))) | ||
Theorem | sxval 29580* | Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ 𝐴 = ran (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑇 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ×s 𝑇) = (sigaGen‘𝐴)) | ||
Theorem | sxsiga 29581 | A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra) | ||
Theorem | sxsigon 29582 | 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 29583 | The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) | ||
Theorem | elsx 29584 | 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 29585 | Extend class notation to include the class of measures. |
class measures | ||
Definition | df-meas 29586* | 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 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) | ||
Theorem | measbase 29587 | The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran sigAlgebra) | ||
Theorem | measval 29588* | The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (measures‘𝑆) = {𝑚 ∣ (𝑚:𝑆⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) | ||
Theorem | ismeas 29589* | The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 19-Oct-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀 ∈ (measures‘𝑆) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) | ||
Theorem | isrnmeas 29590* | The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝑀 ∈ ∪ ran measures → (dom 𝑀 ∈ ∪ ran sigAlgebra ∧ (𝑀:dom 𝑀⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) | ||
Theorem | dmmeas 29591 | The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra) | ||
Theorem | measbasedom 29592 | The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀)) | ||
Theorem | measfrge0 29593 | A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞)) | ||
Theorem | measfn 29594 | A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀 Fn 𝑆) | ||
Theorem | measvxrge0 29595 | The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑀‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | measvnul 29596 | The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0) | ||
Theorem | measge0 29597 | A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝑀‘𝐴)) | ||
Theorem | measle0 29598 | If the measure of a given set is bounded by zero, it is zero. (Contributed by Thierry Arnoux, 20-Oct-2017.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ≤ 0) → (𝑀‘𝐴) = 0) | ||
Theorem | measvun 29599* | The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑀‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑀‘𝑥)) | ||
Theorem | measxun2 29600 | The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐵 ⊆ 𝐴) → (𝑀‘𝐴) = ((𝑀‘𝐵) +𝑒 (𝑀‘(𝐴 ∖ 𝐵)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |