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