![]() |
Metamath
Proof Explorer Theorem List (p. 332 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | csiga 33101 | Extend class notation to include the function giving the sigma-algebras on a given base set. |
class sigAlgebra | ||
Definition | df-siga 33102* | 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 33103* | Lemma for issiga 33105 and isrnsiga 33106. The class of sigma-algebras with base set π is a set. Note: a more generic version with (π β V β ...) could be useful for sigaval 33104. (Contributed by Thierry Arnoux, 24-Oct-2016.) |
β’ {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯ β π )))} β V | ||
Theorem | sigaval 33104* | The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.) |
β’ (π β V β (sigAlgebraβπ) = {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯ β π )))}) | ||
Theorem | issiga 33105* | An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
β’ (π β V β (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯ β π))))) | ||
Theorem | isrnsiga 33106* | 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 33107 | A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
β’ (π β βͺ ran sigAlgebra β β β π) | ||
Theorem | baselsiga 33108 | A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.) |
β’ (π β (sigAlgebraβπ΄) β π΄ β π) | ||
Theorem | sigasspw 33109 | A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.) |
β’ (π β (sigAlgebraβπ΄) β π β π« π΄) | ||
Theorem | sigaclcu 33110 | A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π« π β§ π΄ βΌ Ο) β βͺ π΄ β π) | ||
Theorem | sigaclcuni 33111* | A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
β’ β²ππ΄ β β’ ((π β βͺ ran sigAlgebra β§ βπ β π΄ π΅ β π β§ π΄ βΌ Ο) β βͺ π β π΄ π΅ β π) | ||
Theorem | sigaclfu 33112 | A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π« π β§ π΄ β Fin) β βͺ π΄ β π) | ||
Theorem | sigaclcu2 33113* | A sigma-algebra is closed under countable union - indexing on β (Contributed by Thierry Arnoux, 29-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ βπ β β π΄ β π) β βͺ π β β π΄ β π) | ||
Theorem | sigaclfu2 33114* | A sigma-algebra is closed under finite union - indexing on (1..^π). (Contributed by Thierry Arnoux, 28-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ βπ β (1..^π)π΄ β π) β βͺ π β (1..^π)π΄ β π) | ||
Theorem | sigaclcu3 33115* | A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.) |
β’ (π β π β βͺ ran sigAlgebra) & β’ (π β (π = β β¨ π = (1..^π))) & β’ ((π β§ π β π) β π΄ β π) β β’ (π β βͺ π β π π΄ β π) | ||
Theorem | issgon 33116 | 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 33117 | A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
β’ (π β βͺ ran sigAlgebra β π β (sigAlgebraββͺ π)) | ||
Theorem | elsigass 33118 | An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β π΄ β βͺ π) | ||
Theorem | elrnsiga 33119 | Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
β’ (π β (sigAlgebraβπ) β π β βͺ ran sigAlgebra) | ||
Theorem | isrnsigau 33120* | The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.) |
β’ (π β βͺ ran sigAlgebra β (π β π« βͺ π β§ (βͺ π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯ β π)))) | ||
Theorem | unielsiga 33121 | 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 33122 | 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 33123 | Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
β’ (π β π β π« π β (sigAlgebraβπ)) | ||
Theorem | prsiga 33124 | The smallest possible sigma-algebra containing π. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
β’ (π β π β {β , π} β (sigAlgebraβπ)) | ||
Theorem | sigaclci 33125 | A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π« π) β§ (π΄ βΌ Ο β§ π΄ β β )) β β© π΄ β π) | ||
Theorem | difelsiga 33126 | A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) β π) | ||
Theorem | unelsiga 33127 | A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) | ||
Theorem | inelsiga 33128 | A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | sigainb 33129 | Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β (π β© π« π΄) β (sigAlgebraβπ΄)) | ||
Theorem | insiga 33130 | 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 33131 | Extend class notation to include the sigma-algebra generator. |
class sigaGen | ||
Definition | df-sigagen 33132* | 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 33133* | Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ (π΄ β π β (sigaGenβπ΄) = β© {π β (sigAlgebraββͺ π΄) β£ π΄ β π }) | ||
Theorem | sigagensiga 33134 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ (π΄ β π β (sigaGenβπ΄) β (sigAlgebraββͺ π΄)) | ||
Theorem | sgsiga 33135 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ (π β π΄ β π) β β’ (π β (sigaGenβπ΄) β βͺ ran sigAlgebra) | ||
Theorem | unisg 33136 | The sigma-algebra generated by a collection π΄ is a sigma-algebra on βͺ π΄. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ (π΄ β π β βͺ (sigaGenβπ΄) = βͺ π΄) | ||
Theorem | dmsigagen 33137 | A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ dom sigaGen = V | ||
Theorem | sssigagen 33138 | A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.) |
β’ (π΄ β π β π΄ β (sigaGenβπ΄)) | ||
Theorem | sssigagen2 33139 | 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 33140 | 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 33141 | 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 33142 | 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 33143 | 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 33144 | 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 33145* | The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } β β’ (π β π β (π β π« π« π β§ (fiβπ) β π)) | ||
Theorem | ispisys2 33146* | 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 33147* | Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | sigapisys 33148* | All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } β β’ (sigAlgebraβπ) β π | ||
Theorem | isldsys 33149* | 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 33150* | The power set of the universe set π is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} β β’ (π β π β π« π β πΏ) | ||
Theorem | unelldsys 33151* | Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | sigaldsys 33152* | All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} β β’ (sigAlgebraβπ) β πΏ | ||
Theorem | ldsysgenld 33153* | 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 33154* | Lemma for sigapildsys 33155. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ β²ππ & β’ (π β π‘ β (π β© πΏ)) & β’ (π β π΄ β π‘) & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΅ β π‘) β β’ (π β (π΄ β βͺ π β π π΅) β π‘) | ||
Theorem | sigapildsys 33155* | Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} β β’ (sigAlgebraβπ) = (π β© πΏ) | ||
Theorem | ldgenpisyslem1 33156* | Lemma for ldgenpisys 33159. (Contributed by Thierry Arnoux, 29-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) & β’ (π β π΄ β πΈ) β β’ (π β {π β π« π β£ (π΄ β© π) β πΈ} β πΏ) | ||
Theorem | ldgenpisyslem2 33157* | Lemma for ldgenpisys 33159. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) & β’ (π β π΄ β πΈ) & β’ (π β π β {π β π« π β£ (π΄ β© π) β πΈ}) β β’ (π β πΈ β {π β π« π β£ (π΄ β© π) β πΈ}) | ||
Theorem | ldgenpisyslem3 33158* | Lemma for ldgenpisys 33159. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β πΈ β {π β π« π β£ (π΄ β© π) β πΈ}) | ||
Theorem | ldgenpisys 33159* | The lambda system πΈ generated by a pi-system π is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) β β’ (π β πΈ β π) | ||
Theorem | dynkin 33160* | 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 33161* | 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 33162* | A ring of sets is a collection of subsets of π. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ (π β π β π β π« π) | ||
Theorem | 0elros 33163* | A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ (π β π β β β π) | ||
Theorem | unelros 33164* | A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) | ||
Theorem | difelros 33165* | A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) β π) | ||
Theorem | inelros 33166* | A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | fiunelros 33167* | A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} & β’ (π β π β π) & β’ (π β π β β) & β’ ((π β§ π β (1..^π)) β π΅ β π) β β’ (π β βͺ π β (1..^π)π΅ β π) | ||
Theorem | issros 33168* | 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 33169* | A semiring of sets is a collection of subsets of π. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ (π β π β π β π« π) | ||
Theorem | 0elsros 33170* | A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ (π β π β β β π) | ||
Theorem | inelsros 33171* | A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | diffiunisros 33172* | 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 33173* | Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} & β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ (π β π β π β π) | ||
Syntax | cbrsiga 33174 | The Borel Algebra on real numbers, usually a gothic B |
class π β | ||
Definition | df-brsiga 33175 | 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 33176 | The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ π β β (sigaGen β Top) | ||
Theorem | brsigarn 33177 | The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ π β β (sigAlgebraββ) | ||
Theorem | brsigasspwrn 33178 | The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
β’ π β β π« β | ||
Theorem | unibrsiga 33179 | The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ βͺ π β = β | ||
Theorem | cldssbrsiga 33180 | A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.) |
β’ (π½ β Top β (Clsdβπ½) β (sigaGenβπ½)) | ||
Syntax | csx 33181 | Extend class notation with the product sigma-algebra operation. |
class Γs | ||
Definition | df-sx 33182* | Define the product sigma-algebra operation, analogous to df-tx 23065. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ Γs = (π β V, π‘ β V β¦ (sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)))) | ||
Theorem | sxval 33183* | Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ π΄ = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β β’ ((π β π β§ π β π) β (π Γs π) = (sigaGenβπ΄)) | ||
Theorem | sxsiga 33184 | A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran sigAlgebra) β (π Γs π) β βͺ ran sigAlgebra) | ||
Theorem | sxsigon 33185 | 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 33186 | The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran sigAlgebra) β (βͺ π Γ βͺ π) = βͺ (π Γs π)) | ||
Theorem | elsx 33187 | 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 33188 | Extend class notation to include the class of measures. |
class measures | ||
Definition | df-meas 33189* | 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 33190 | The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β (measuresβπ) β π β βͺ ran sigAlgebra) | ||
Theorem | measval 33191* | 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 33192* | 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 33193* | 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 33194 | The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
β’ (π β βͺ ran measures β dom π β βͺ ran sigAlgebra) | ||
Theorem | measbasedom 33195 | The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β βͺ ran measures β π β (measuresβdom π)) | ||
Theorem | measfrge0 33196 | A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ (π β (measuresβπ) β π:πβΆ(0[,]+β)) | ||
Theorem | measfn 33197 | A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
β’ (π β (measuresβπ) β π Fn π) | ||
Theorem | measvxrge0 33198 | The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π) β (πβπ΄) β (0[,]+β)) | ||
Theorem | measvnul 33199 | The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ (π β (measuresβπ) β (πββ ) = 0) | ||
Theorem | measge0 33200 | A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
β’ ((π β (measuresβπ) β§ π΄ β π) β 0 β€ (πβπ΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |