Home | Metamath
Proof Explorer Theorem List (p. 326 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sigagensiga 32501 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ (π΄ β π β (sigaGenβπ΄) β (sigAlgebraββͺ π΄)) | ||
Theorem | sgsiga 32502 | A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ (π β π΄ β π) β β’ (π β (sigaGenβπ΄) β βͺ ran sigAlgebra) | ||
Theorem | unisg 32503 | The sigma-algebra generated by a collection π΄ is a sigma-algebra on βͺ π΄. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ (π΄ β π β βͺ (sigaGenβπ΄) = βͺ π΄) | ||
Theorem | dmsigagen 32504 | A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ dom sigaGen = V | ||
Theorem | sssigagen 32505 | A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.) |
β’ (π΄ β π β π΄ β (sigaGenβπ΄)) | ||
Theorem | sssigagen2 32506 | 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 32507 | 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 32508 | 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 32509 | 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 32510 | 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 32511 | 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 32512* | The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } β β’ (π β π β (π β π« π« π β§ (fiβπ) β π)) | ||
Theorem | ispisys2 32513* | 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 32514* | Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | sigapisys 32515* | All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } β β’ (sigAlgebraβπ) β π | ||
Theorem | isldsys 32516* | 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 32517* | The power set of the universe set π is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} β β’ (π β π β π« π β πΏ) | ||
Theorem | unelldsys 32518* | Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | sigaldsys 32519* | All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} β β’ (sigAlgebraβπ) β πΏ | ||
Theorem | ldsysgenld 32520* | 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 32521* | Lemma for sigapildsys 32522. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ β²ππ & β’ (π β π‘ β (π β© πΏ)) & β’ (π β π΄ β π‘) & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΅ β π‘) β β’ (π β (π΄ β βͺ π β π π΅) β π‘) | ||
Theorem | sigapildsys 32522* | Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} β β’ (sigAlgebraβπ) = (π β© πΏ) | ||
Theorem | ldgenpisyslem1 32523* | Lemma for ldgenpisys 32526. (Contributed by Thierry Arnoux, 29-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) & β’ (π β π΄ β πΈ) β β’ (π β {π β π« π β£ (π΄ β© π) β πΈ} β πΏ) | ||
Theorem | ldgenpisyslem2 32524* | Lemma for ldgenpisys 32526. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) & β’ (π β π΄ β πΈ) & β’ (π β π β {π β π« π β£ (π΄ β© π) β πΈ}) β β’ (π β πΈ β {π β π« π β£ (π΄ β© π) β πΈ}) | ||
Theorem | ldgenpisyslem3 32525* | Lemma for ldgenpisys 32526. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β πΈ β {π β π« π β£ (π΄ β© π) β πΈ}) | ||
Theorem | ldgenpisys 32526* | The lambda system πΈ generated by a pi-system π is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.) |
β’ π = {π β π« π« π β£ (fiβπ ) β π } & β’ πΏ = {π β π« π« π β£ (β β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} & β’ (π β π β π) & β’ πΈ = β© {π‘ β πΏ β£ π β π‘} & β’ (π β π β π) β β’ (π β πΈ β π) | ||
Theorem | dynkin 32527* | 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 32528* | 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 32529* | A ring of sets is a collection of subsets of π. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ (π β π β π β π« π) | ||
Theorem | 0elros 32530* | A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ (π β π β β β π) | ||
Theorem | unelros 32531* | A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) | ||
Theorem | difelros 32532* | A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) β π) | ||
Theorem | inelros 32533* | A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | fiunelros 32534* | A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} & β’ (π β π β π) & β’ (π β π β β) & β’ ((π β§ π β (1..^π)) β π΅ β π) β β’ (π β βͺ π β (1..^π)π΅ β π) | ||
Theorem | issros 32535* | 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 32536* | A semiring of sets is a collection of subsets of π. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ (π β π β π β π« π) | ||
Theorem | 0elsros 32537* | A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ (π β π β β β π) | ||
Theorem | inelsros 32538* | A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β π) | ||
Theorem | diffiunisros 32539* | 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 32540* | Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.) |
β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ βͺ π¦) β π β§ (π₯ β π¦) β π ))} & β’ π = {π β π« π« π β£ (β β π β§ βπ₯ β π βπ¦ β π ((π₯ β© π¦) β π β§ βπ§ β π« π (π§ β Fin β§ Disj π‘ β π§ π‘ β§ (π₯ β π¦) = βͺ π§)))} β β’ (π β π β π β π) | ||
Syntax | cbrsiga 32541 | The Borel Algebra on real numbers, usually a gothic B |
class π β | ||
Definition | df-brsiga 32542 | 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 32543 | The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ π β β (sigaGen β Top) | ||
Theorem | brsigarn 32544 | The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ π β β (sigAlgebraββ) | ||
Theorem | brsigasspwrn 32545 | The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
β’ π β β π« β | ||
Theorem | unibrsiga 32546 | The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ βͺ π β = β | ||
Theorem | cldssbrsiga 32547 | A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.) |
β’ (π½ β Top β (Clsdβπ½) β (sigaGenβπ½)) | ||
Syntax | csx 32548 | Extend class notation with the product sigma-algebra operation. |
class Γs | ||
Definition | df-sx 32549* | Define the product sigma-algebra operation, analogous to df-tx 22835. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ Γs = (π β V, π‘ β V β¦ (sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)))) | ||
Theorem | sxval 32550* | Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ π΄ = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β β’ ((π β π β§ π β π) β (π Γs π) = (sigaGenβπ΄)) | ||
Theorem | sxsiga 32551 | A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran sigAlgebra) β (π Γs π) β βͺ ran sigAlgebra) | ||
Theorem | sxsigon 32552 | 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 32553 | The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.) |
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran sigAlgebra) β (βͺ π Γ βͺ π) = βͺ (π Γs π)) | ||
Theorem | elsx 32554 | 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 32555 | Extend class notation to include the class of measures. |
class measures | ||
Definition | df-meas 32556* | 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 32557 | The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β (measuresβπ) β π β βͺ ran sigAlgebra) | ||
Theorem | measval 32558* | 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 32559* | 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 32560* | 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 32561 | The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.) |
β’ (π β βͺ ran measures β dom π β βͺ ran sigAlgebra) | ||
Theorem | measbasedom 32562 | The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β βͺ ran measures β π β (measuresβdom π)) | ||
Theorem | measfrge0 32563 | A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ (π β (measuresβπ) β π:πβΆ(0[,]+β)) | ||
Theorem | measfn 32564 | A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
β’ (π β (measuresβπ) β π Fn π) | ||
Theorem | measvxrge0 32565 | The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π) β (πβπ΄) β (0[,]+β)) | ||
Theorem | measvnul 32566 | The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ (π β (measuresβπ) β (πββ ) = 0) | ||
Theorem | measge0 32567 | A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
β’ ((π β (measuresβπ) β§ π΄ β π) β 0 β€ (πβπ΄)) | ||
Theorem | measle0 32568 | 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 32569* | The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π« π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) β (πββͺ π΄) = Ξ£*π₯ β π΄(πβπ₯)) | ||
Theorem | measxun2 32570 | The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.) |
β’ ((π β (measuresβπ) β§ (π΄ β π β§ π΅ β π) β§ π΅ β π΄) β (πβπ΄) = ((πβπ΅) +π (πβ(π΄ β π΅)))) | ||
Theorem | measun 32571 | The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.) |
β’ ((π β (measuresβπ) β§ (π΄ β π β§ π΅ β π) β§ (π΄ β© π΅) = β ) β (πβ(π΄ βͺ π΅)) = ((πβπ΄) +π (πβπ΅))) | ||
Theorem | measvunilem 32572* | Lemma for measvuni 32574. (Contributed by Thierry Arnoux, 7-Feb-2017.) (Revised by Thierry Arnoux, 19-Feb-2017.) (Revised by Thierry Arnoux, 6-Mar-2017.) |
β’ β²π₯π΄ β β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β }) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ π₯ β π΄ π΅) = Ξ£*π₯ β π΄(πβπ΅)) | ||
Theorem | measvunilem0 32573* | Lemma for measvuni 32574. (Contributed by Thierry Arnoux, 6-Mar-2017.) |
β’ β²π₯π΄ β β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β {β } β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ π₯ β π΄ π΅) = Ξ£*π₯ β π΄(πβπ΅)) | ||
Theorem | measvuni 32574* | The measure of a countable disjoint union is the sum of the measures. This theorem uses a collection rather than a set of subsets of π. (Contributed by Thierry Arnoux, 7-Mar-2017.) |
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ π₯ β π΄ π΅) = Ξ£*π₯ β π΄(πβπ΅)) | ||
Theorem | measssd 32575 | A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
β’ (π β π β (measuresβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) β β’ (π β (πβπ΄) β€ (πβπ΅)) | ||
Theorem | measunl 32576 | A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017.) |
β’ (π β π β (measuresβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (πβ(π΄ βͺ π΅)) β€ ((πβπ΄) +π (πβπ΅))) | ||
Theorem | measiuns 32577* | The measure of the union of a collection of sets, expressed as the sum of a disjoint set. This is used as a lemma for both measiun 32578 and meascnbl 32579. (Contributed by Thierry Arnoux, 22-Jan-2017.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) & β’ (π β (π = β β¨ π = (1..^πΌ))) & β’ (π β π β (measuresβπ)) & β’ ((π β§ π β π) β π΄ β π) β β’ (π β (πββͺ π β π π΄) = Ξ£*π β π(πβ(π΄ β βͺ π β (1..^π)π΅))) | ||
Theorem | measiun 32578* | A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.) |
β’ (π β π β (measuresβπ)) & β’ (π β π΄ β π) & β’ ((π β§ π β β) β π΅ β π) & β’ (π β π΄ β βͺ π β β π΅) β β’ (π β (πβπ΄) β€ Ξ£*π β β(πβπ΅)) | ||
Theorem | meascnbl 32579* | A measure is continuous from below. Cf. volsup 24842. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.) |
β’ π½ = (TopOpenβ(β*π βΎs (0[,]+β))) & β’ (π β π β (measuresβπ)) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β (πΉβπ) β (πΉβ(π + 1))) β β’ (π β (π β πΉ)(βπ‘βπ½)(πββͺ ran πΉ)) | ||
Theorem | measinblem 32580* | Lemma for measinb 32581. (Contributed by Thierry Arnoux, 2-Jun-2017.) |
β’ ((((π β (measuresβπ) β§ π΄ β π) β§ π΅ β π« π) β§ (π΅ βΌ Ο β§ Disj π₯ β π΅ π₯)) β (πβ(βͺ π΅ β© π΄)) = Ξ£*π₯ β π΅(πβ(π₯ β© π΄))) | ||
Theorem | measinb 32581* | Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π) β (π₯ β π β¦ (πβ(π₯ β© π΄))) β (measuresβπ)) | ||
Theorem | measres 32582 | Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π β βͺ ran sigAlgebra β§ π β π) β (π βΎ π) β (measuresβπ)) | ||
Theorem | measinb2 32583* | Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π) β (π₯ β (π β© π« π΄) β¦ (πβ(π₯ β© π΄))) β (measuresβ(π β© π« π΄))) | ||
Theorem | measdivcst 32584 | Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π βf/c /π π΄) β (measuresβπ)) | ||
Theorem | measdivcstALTV 32585* | Alternate version of measdivcst 32584. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.) |
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ)) | ||
Theorem | cntmeas 32586 | The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β βͺ ran sigAlgebra β (β― βΎ π) β (measuresβπ)) | ||
Theorem | pwcntmeas 32587 | The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017.) |
β’ (π β π β (β― βΎ π« π) β (measuresβπ« π)) | ||
Theorem | cntnevol 32588 | Counting and Lebesgue measures are different. (Contributed by Thierry Arnoux, 27-Jan-2017.) |
β’ (β― βΎ π« π) β vol | ||
Theorem | voliune 32589 | The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +β for the measure of any set in the sum. Cf. ovoliun 24791 and voliun 24840. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
β’ ((βπ β β π΄ β dom vol β§ Disj π β β π΄) β (volββͺ π β β π΄) = Ξ£*π β β(volβπ΄)) | ||
Theorem | volfiniune 32590* | The Lebesgue measure function is countably additive. This theorem is to volfiniun 24833 what voliune 32589 is to voliun 24840. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β dom vol β§ Disj π β π΄ π΅) β (volββͺ π β π΄ π΅) = Ξ£*π β π΄(volβπ΅)) | ||
Theorem | volmeas 32591 | The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
β’ vol β (measuresβdom vol) | ||
Syntax | cdde 32592 | Extend class notation to include the Dirac delta measure. |
class Ξ΄ | ||
Definition | df-dde 32593 | Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
β’ Ξ΄ = (π β π« β β¦ if(0 β π, 1, 0)) | ||
Theorem | ddeval1 32594 | Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
β’ ((π΄ β β β§ 0 β π΄) β (Ξ΄βπ΄) = 1) | ||
Theorem | ddeval0 32595 | Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
β’ ((π΄ β β β§ Β¬ 0 β π΄) β (Ξ΄βπ΄) = 0) | ||
Theorem | ddemeas 32596 | The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
β’ Ξ΄ β (measuresβπ« β) | ||
Syntax | cae 32597 | Extend class notation to include the 'almost everywhere' relation. |
class a.e. | ||
Syntax | cfae 32598 | Extend class notation to include the 'almost everywhere' builder. |
class ~ a.e. | ||
Definition | df-ae 32599* | Define 'almost everywhere' with regard to a measure π. A property holds almost everywhere if the measure of the set where it does not hold has measure zero. (Contributed by Thierry Arnoux, 20-Oct-2017.) |
β’ a.e. = {β¨π, πβ© β£ (πβ(βͺ dom π β π)) = 0} | ||
Theorem | relae 32600 | 'almost everywhere' is a relation. (Contributed by Thierry Arnoux, 20-Oct-2017.) |
β’ Rel a.e. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |