P. 303 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30201-30300   *Has distinct variable group(s)

Type	Label	Description
Statement
20.3.16.2  Generated sigma-Algebra
Syntax	csigagen 30201	Extend class notation to include the sigma-algebra generator.
class sigaGen
Definition	df-sigagen 30202*	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 = ( x e. _V |-> |^| { s e. (sigAlgebra ` U. x ) | x C_ s } )
Theorem	sigagenval 30203*	Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( A e. V -> (sigaGen ` A ) = |^| { s e. (sigAlgebra ` U. A ) | A C_ s } )
Theorem	sigagensiga 30204	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( A e. V -> (sigaGen ` A ) e. (sigAlgebra ` U. A ) )
Theorem	sgsiga 30205	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> A e. V )   =>    |- ( ph -> (sigaGen ` A ) e. U. ran sigAlgebra )
Theorem	unisg 30206	The sigma-algebra generated by a collection A is a sigma-algebra on U. A. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( A e. V -> U. (sigaGen ` A ) = U. A )
Theorem	dmsigagen 30207	A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- dom sigaGen = _V
Theorem	sssigagen 30208	A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.)
|- ( A e. V -> A C_ (sigaGen ` A ) )
Theorem	sssigagen2 30209	A subset of the generating set is also a subset of the generated sigma-algebra. (Contributed by Thierry Arnoux, 22-Sep-2017.)
|- ( ( A e. V /\ B C_ A ) -> B C_ (sigaGen ` A ) )
Theorem	elsigagen 30210	Any element of a set is also an element of the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 27-Mar-2017.)
|- ( ( A e. V /\ B e. A ) -> B e. (sigaGen ` A ) )
Theorem	elsigagen2 30211	Any countable union of elements of a set is also in the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017.)
|- ( ( A e. V /\ B C_ A /\ B ~<_ om ) -> U. B e. (sigaGen ` A ) )
Theorem	sigagenss 30212	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 A. (Contributed by Thierry Arnoux, 4-Jun-2017.)
|- ( ( S e. (sigAlgebra ` U. A ) /\ A C_ S ) -> (sigaGen ` A ) C_ S )
Theorem	sigagenss2 30213	Sufficient condition for inclusion of sigma-algebras. This is used to prove equality of sigma-algebras. (Contributed by Thierry Arnoux, 10-Oct-2017.)
|- ( ( U. A = U. B /\ A C_ (sigaGen ` B ) /\ B e. V ) -> (sigaGen ` A ) C_ (sigaGen ` B ) )
Theorem	sigagenid 30214	The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017.)
|- ( S e. U. ran sigAlgebra -> (sigaGen ` S ) = S )
20.3.16.3  lambda and pi-Systems, Rings of Sets 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 P and L respectively as the classes of pi- and lambda-systems in O throughout this section.
Theorem	ispisys 30215*	The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   =>    |- ( S e. P <-> ( S e. ~P ~P O /\ ( fi ` S ) C_ S ) )
Theorem	ispisys2 30216*	The property of being a pi-system, expanded version. Pi-systems are closed under finite intersections. (Contributed by Thierry Arnoux, 13-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   =>    |- ( S e. P <-> ( S e. ~P ~P O /\ A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )
Theorem	inelpisys 30217*	Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   =>    |- ( ( S e. P /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )
Theorem	sigapisys 30218*	All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   =>    |- (sigAlgebra ` O ) C_ P
Theorem	isldsys 30219*	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.)
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   =>    |- ( S e. L <-> ( S e. ~P ~P O /\ ( (/) e. S /\ A. x e. S ( O \ x ) e. S /\ A. x e. ~P S ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. S ) ) ) )
Theorem	pwldsys 30220*	The power set of the universe set O is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   =>    |- ( O e. V -> ~P O e. L )
Theorem	unelldsys 30221*	Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> S e. L )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> ( A i^i B ) = (/) )   =>    |- ( ph -> ( A u. B ) e. S )
Theorem	sigaldsys 30222*	All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   =>    |- (sigAlgebra ` O ) C_ L
Theorem	ldsysgenld 30223*	The intersection of all lambda-systems containing a given collection of sets A, which is called the lambda-system generated by A, is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> O e. V )   &    |- ( ph -> A C_ ~P O )   =>    |- ( ph -> |^| { t e. L | A C_ t } e. L )
Theorem	sigapildsyslem 30224*	Lemma for sigapildsys 30225. (Contributed by Thierry Arnoux, 13-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- F/ n ph   &    |- ( ph -> t e. ( P i^i L ) )   &    |- ( ph -> A e. t )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ n e. N ) -> B e. t )   =>    |- ( ph -> ( A \ U_ n e. N B ) e. t )
Theorem	sigapildsys 30225*	Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   =>    |- (sigAlgebra ` O ) = ( P i^i L )
Theorem	ldgenpisyslem1 30226*	Lemma for ldgenpisys 30229. (Contributed by Thierry Arnoux, 29-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> O e. V )   &    |- E = |^| { t e. L | T C_ t }   &    |- ( ph -> T e. P )   &    |- ( ph -> A e. E )   =>    |- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. L )
Theorem	ldgenpisyslem2 30227*	Lemma for ldgenpisys 30229. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> O e. V )   &    |- E = |^| { t e. L | T C_ t }   &    |- ( ph -> T e. P )   &    |- ( ph -> A e. E )   &    |- ( ph -> T C_ { b e. ~P O | ( A i^i b ) e. E } )   =>    |- ( ph -> E C_ { b e. ~P O | ( A i^i b ) e. E } )
Theorem	ldgenpisyslem3 30228*	Lemma for ldgenpisys 30229. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> O e. V )   &    |- E = |^| { t e. L | T C_ t }   &    |- ( ph -> T e. P )   &    |- ( ph -> A e. T )   =>    |- ( ph -> E C_ { b e. ~P O | ( A i^i b ) e. E } )
Theorem	ldgenpisys 30229*	The lambda system E generated by a pi-system T is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> O e. V )   &    |- E = |^| { t e. L | T C_ t }   &    |- ( ph -> T e. P )   =>    |- ( ph -> E e. P )
Theorem	dynkin 30230*	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.)
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }   &    |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }   &    |- ( ph -> O e. V )   &    |- ( ph -> S e. L )   &    |- ( ph -> T e. P )   &    |- ( ph -> T C_ S )   =>    |- ( ph -> |^| { u e. (sigAlgebra ` O ) | T C_ u } C_ S )
Theorem	isros 30231*	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.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   =>    |- ( S e. Q <-> ( S e. ~P ~P O /\ (/) e. S /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) )
Theorem	rossspw 30232*	A ring of sets is a collection of subsets of O. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   =>    |- ( S e. Q -> S C_ ~P O )
Theorem	0elros 30233*	A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   =>    |- ( S e. Q -> (/) e. S )
Theorem	unelros 30234*	A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   =>    |- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A u. B ) e. S )
Theorem	difelros 30235*	A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   =>    |- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )
Theorem	inelros 30236*	A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   =>    |- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )
Theorem	fiunelros 30237*	A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   &    |- ( ph -> S e. Q )   &    |- ( ph -> N e. NN )   &    |- ( ( ph /\ k e. ( 1..^ N ) ) -> B e. S )   =>    |- ( ph -> U_ k e. ( 1..^ N ) B e. S )
Theorem	issros 30238*	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.)
|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) }   =>    |- ( S e. N <-> ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) )
Theorem	srossspw 30239*	A semi-ring of sets is a collection of subsets of O. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) }   =>    |- ( S e. N -> S C_ ~P O )
Theorem	0elsros 30240*	A semi-ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) }   =>    |- ( S e. N -> (/) e. S )
Theorem	inelsros 30241*	A semi-ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) }   =>    |- ( ( S e. N /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )
Theorem	diffiunisros 30242*	In semiring of sets, complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) }   =>    |- ( ( S e. N /\ A e. S /\ B e. S ) -> E. z e. ~P S ( z e. Fin /\ Disj t e. z t /\ ( A \ B ) = U. z ) )
Theorem	rossros 30243*	Rings of sets are semi-rings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.)
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }   &    |- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj t e. z t /\ ( x \ y ) = U. z ) ) ) }   =>    |- ( S e. Q -> S e. N )
20.3.16.4  The Borel algebra on the real numbers
Syntax	cbrsiga 30244	The Borel Algebra on real numbers, usually a gothic B
class 𝔅ℝ
Definition	df-brsiga 30245	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 J is the sigma-algebra generated by J, (sigaGen ` J ), 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 30246	The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- 𝔅ℝ e. (sigaGen " Top )
Theorem	brsigarn 30247	The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- 𝔅ℝ e. (sigAlgebra ` RR )
Theorem	brsigasspwrn 30248	The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.)
|- 𝔅ℝ C_ ~P RR
Theorem	unibrsiga 30249	The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- U.𝔅ℝ = RR
Theorem	cldssbrsiga 30250	A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.)
|- ( J e. Top -> ( Clsd ` J ) C_ (sigaGen ` J ) )
20.3.16.5  Product Sigma-Algebra
Syntax	csx 30251	Extend class notation with the product sigma-algebra operation.
class ×s
Definition	df-sx 30252*	Define the product sigma-algebra operation, analogous to df-tx 21365. (Contributed by Thierry Arnoux, 1-Jun-2017.)
|- ×s = ( s e. _V , t e. _V |-> (sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )
Theorem	sxval 30253*	Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.)
|- A = ran ( x e. S , y e. T |-> ( x X. y ) )   =>    |- ( ( S e. V /\ T e. W ) -> ( S ×s T ) = (sigaGen ` A ) )
Theorem	sxsiga 30254	A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S ×s T ) e. U. ran sigAlgebra )
Theorem	sxsigon 30255	A product sigma-algebra is a sigma-algebra on the product of the bases. (Contributed by Thierry Arnoux, 1-Jun-2017.)
|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S ×s T ) e. (sigAlgebra ` ( U. S X. U. T ) ) )
Theorem	sxuni 30256	The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S ×s T ) )
Theorem	elsx 30257	The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
|- ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ( A X. B ) e. ( S ×s T ) )
20.3.16.6  Measures
Syntax	cmeas 30258	Extend class notation to include the class of measures.
class measures
Definition	df-meas 30259*	Define a measure as a nonnegative countably additive function over a sigma-algebra onto ( 0 [,] +oo ). (Contributed by Thierry Arnoux, 10-Sep-2016.)
|- measures = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) ) } )
Theorem	measbase 30260	The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( M e. (measures ` S ) -> S e. U. ran sigAlgebra )
Theorem	measval 30261*	The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016.)
|- ( S e. U. ran sigAlgebra -> (measures ` S ) = { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ om /\ Disj y e. x y ) -> ( m ` U. x ) = Σ* y e. x ( m ` y ) ) ) } )
Theorem	ismeas 30262*	The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 19-Oct-2016.)
|- ( S e. U. ran sigAlgebra -> ( M e. (measures ` S ) <-> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ om /\ Disj y e. x y ) -> ( M ` U. x ) = Σ* y e. x ( M ` y ) ) ) ) )
Theorem	isrnmeas 30263*	The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( M e. U. ran measures -> ( dom M e. U. ran sigAlgebra /\ ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ om /\ Disj y e. x y ) -> ( M ` U. x ) = Σ* y e. x ( M ` y ) ) ) ) )
Theorem	dmmeas 30264	The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.)
|- ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
Theorem	measbasedom 30265	The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( M e. U. ran measures <-> M e. (measures ` dom M ) )
Theorem	measfrge0 30266	A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
|- ( M e. (measures ` S ) -> M : S --> ( 0 [,] +oo ) )
Theorem	measfn 30267	A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
|- ( M e. (measures ` S ) -> M Fn S )
Theorem	measvxrge0 30268	The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
|- ( ( M e. (measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )
Theorem	measvnul 30269	The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.)
|- ( M e. (measures ` S ) -> ( M ` (/) ) = 0 )
Theorem	measge0 30270	A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.)
|- ( ( M e. (measures ` S ) /\ A e. S ) -> 0 <_ ( M ` A ) )
Theorem	measle0 30271	If the measure of a given set is bounded by zero, it is zero. (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- ( ( M e. (measures ` S ) /\ A e. S /\ ( M ` A ) <_ 0 ) -> ( M ` A ) = 0 )
Theorem	measvun 30272*	The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.)
|- ( ( M e. (measures ` S ) /\ A e. ~P S /\ ( A ~<_ om /\ Disj x e. A x ) ) -> ( M ` U. A ) = Σ* x e. A ( M ` x ) )
Theorem	measxun2 30273	The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
|- ( ( M e. (measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` A ) = ( ( M ` B ) +e ( M ` ( A \ B ) ) ) )
Theorem	measun 30274	The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
|- ( ( M e. (measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )
Theorem	measvunilem 30275*	Lemma for measvuni 30277. (Contributed by Thierry Arnoux, 7-Feb-2017.) (Revised by Thierry Arnoux, 19-Feb-2017.) (Revised by Thierry Arnoux, 6-Mar-2017.)
|- F/_ x A   =>    |- ( ( M e. (measures ` S ) /\ A. x e. A B e. ( S \ { (/) } ) /\ ( A ~<_ om /\ Disj x e. A B ) ) -> ( M ` U_ x e. A B ) = Σ* x e. A ( M ` B ) )
Theorem	measvunilem0 30276*	Lemma for measvuni 30277. (Contributed by Thierry Arnoux, 6-Mar-2017.)
|- F/_ x A   =>    |- ( ( M e. (measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ om /\ Disj x e. A B ) ) -> ( M ` U_ x e. A B ) = Σ* x e. A ( M ` B ) )
Theorem	measvuni 30277*	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 S. (Contributed by Thierry Arnoux, 7-Mar-2017.)
|- ( ( M e. (measures ` S ) /\ A. x e. A B e. S /\ ( A ~<_ om /\ Disj x e. A B ) ) -> ( M ` U_ x e. A B ) = Σ* x e. A ( M ` B ) )
Theorem	measssd 30278	A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.)
|- ( ph -> M e. (measures ` S ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> ( M ` A ) <_ ( M ` B ) )
Theorem	measunl 30279	A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- ( ph -> M e. (measures ` S ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   =>    |- ( ph -> ( M ` ( A u. B ) ) <_ ( ( M ` A ) +e ( M ` B ) ) )
Theorem	measiuns 30280*	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 30281 and meascnbl 30282. (Contributed by Thierry Arnoux, 22-Jan-2017.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
|- F/_ n B   &    |- ( n = k -> A = B )   &    |- ( ph -> ( N = NN \/ N = ( 1..^ I ) ) )   &    |- ( ph -> M e. (measures ` S ) )   &    |- ( ( ph /\ n e. N ) -> A e. S )   =>    |- ( ph -> ( M ` U_ n e. N A ) = Σ* n e. N ( M ` ( A \ U_ k e. ( 1..^ n ) B ) ) )
Theorem	measiun 30281*	A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
|- ( ph -> M e. (measures ` S ) )   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ n e. NN ) -> B e. S )   &    |- ( ph -> A C_ U_ n e. NN B )   =>    |- ( ph -> ( M ` A ) <_ Σ* n e. NN ( M ` B ) )
Theorem	meascnbl 30282*	A measure is continuous from below. Cf. volsup 23324. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
|- J = ( TopOpen ` ( RR*s ↾s ( 0 [,] +oo ) ) )   &    |- ( ph -> M e. (measures ` S ) )   &    |- ( ph -> F : NN --> S )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )   =>    |- ( ph -> ( M o. F ) ( ~~> t ` J ) ( M ` U. ran F ) )
Theorem	measinblem 30283*	Lemma for measinb 30284. (Contributed by Thierry Arnoux, 2-Jun-2017.)
|- ( ( ( ( M e. (measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ om /\ Disj x e. B x ) ) -> ( M ` ( U. B i^i A ) ) = Σ* x e. B ( M ` ( x i^i A ) ) )
Theorem	measinb 30284*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( M e. (measures ` S ) /\ A e. S ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) e. (measures ` S ) )
Theorem	measres 30285	Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( M e. (measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( M |` T ) e. (measures ` T ) )
Theorem	measinb2 30286*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( M e. (measures ` S ) /\ A e. S ) -> ( x e. ( S i^i ~P A ) |-> ( M ` ( x i^i A ) ) ) e. (measures ` ( S i^i ~P A ) ) )
Theorem	measdivcstOLD 30287*	Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) e. (measures ` S ) )
Theorem	measdivcst 30288	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.)
|- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( M∘𝑓/𝑐 /𝑒 A ) e. (measures ` S ) )
20.3.16.7  The counting measure
Theorem	cntmeas 30289	The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( S e. U. ran sigAlgebra -> ( # |` S ) e. (measures ` S ) )
Theorem	pwcntmeas 30290	The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017.)
|- ( O e. V -> ( # |` ~P O ) e. (measures ` ~P O ) )
Theorem	cntnevol 30291	Counting and Lebesgue measures are different. (Contributed by Thierry Arnoux, 27-Jan-2017.)
|- ( # |` ~P O ) =/= vol
20.3.16.8  The Lebesgue measure - misc additions
Theorem	voliune 30292	The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +oo for the measure of any set in the sum. Cf. ovoliun 23273 and voliun 23322. (Contributed by Thierry Arnoux, 16-Oct-2017.)
|- ( ( A. n e. NN A e. dom vol /\ Disj n e. NN A ) -> ( vol ` U_ n e. NN A ) = Σ* n e. NN ( vol ` A ) )
Theorem	volfiniune 30293*	The Lebesgue measure function is countably additive. This theorem is to volfiniun 23315 what voliune 30292 is to voliun 23322. (Contributed by Thierry Arnoux, 16-Oct-2017.)
|- ( ( A e. Fin /\ A. n e. A B e. dom vol /\ Disj n e. A B ) -> ( vol ` U_ n e. A B ) = Σ* n e. A ( vol ` B ) )
Theorem	volmeas 30294	The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017.)
|- vol e. (measures ` dom vol )
20.3.16.9  The Dirac delta measure
Syntax	cdde 30295	Extend class notation to include the Dirac delta measure.
class δ
Definition	df-dde 30296	Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- δ = ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )
Theorem	ddeval1 30297	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- ( ( A C_ RR /\ 0 e. A ) -> (δ ` A ) = 1 )
Theorem	ddeval0 30298	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- ( ( A C_ RR /\ -. 0 e. A ) -> (δ ` A ) = 0 )
Theorem	ddemeas 30299	The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- δ e. (measures ` ~P RR )
20.3.16.10  The 'almost everywhere' relation
Syntax	cae 30300	Extend class notation to include the 'almost everywhere' relation.
class a.e.