P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	volfiniune 29101*	The Lebesgue measure function is countably additive. This theorem is to volfiniun 22548 what voliune 29100 is to voliun 22555. (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 29102	The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017.)
|- vol e. (measures ` dom vol )
21.3.15.9  The Dirac delta measure
Syntax	cdde 29103	Extend class notation to include the Dirac delta measure.
class δ
Definition	df-dde 29104	Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- δ = ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )
Theorem	ddeval1 29105	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- ( ( A C_ RR /\ 0 e. A ) -> (δ ` A ) = 1 )
Theorem	ddeval0 29106	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- ( ( A C_ RR /\ -. 0 e. A ) -> (δ ` A ) = 0 )
Theorem	ddemeas 29107	The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
|- δ e. (measures ` ~P RR )
21.3.15.10  The 'almost everywhere' relation
Syntax	cae 29108	Extend class notation to include the 'almost everywhere' relation.
class a.e.
Syntax	cfae 29109	Extend class notation to include the 'almost everywhere' builder.
class ~ a.e.
Definition	df-ae 29110*	Define 'almost everywhere' with regard to a measure M. 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. = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }
Theorem	relae 29111	'almost everywhere' is a relation. (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- Rel a.e.
Theorem	brae 29112	'almost everywhere' relation for a measure and a measurable set A. (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- ( ( M e. U. ran measures /\ A e. dom M ) -> ( Aa.e. M <-> ( M ` ( U. dom M \ A ) ) = 0 ) )
Theorem	braew 29113*	'almost everywhere' relation for a measure M and a property ph (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- U. dom M = O   =>    |- ( M e. U. ran measures -> ( { x e. O | ph }a.e. M <-> ( M ` { x e. O | -. ph } ) = 0 ) )
Theorem	truae 29114*	A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- U. dom M = O   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> ps )   =>    |- ( ph -> { x e. O | ps }a.e. M )
Theorem	aean 29115*	A conjunction holds almost everywhere if and only if both its terms do. (Contributed by Thierry Arnoux, 20-Oct-2017.)
|- U. dom M = O   =>    |- ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( { x e. O | ( ph /\ ps ) }a.e. M <-> ( { x e. O | ph }a.e. M /\ { x e. O | ps }a.e. M ) ) )
Definition	df-fae 29116*	Define a builder for an 'almost everywhere' relation between functions, from relations between function values. In this definition, the range of f and g is enforced in order to ensure the resulting relation is a set. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- ~ a.e. = ( r e. _V , m e. U. ran measures |-> { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m ) } )
Theorem	faeval 29117*	Value of the 'almost everywhere' relation for a given relation and measure. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- ( ( R e. _V /\ M e. U. ran measures ) -> ( R~ a.e. M ) = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) }a.e. M ) } )
Theorem	relfae 29118	The 'almost everywhere' builder for functions produces relations. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- ( ( R e. _V /\ M e. U. ran measures ) -> Rel ( R~ a.e. M ) )
Theorem	brfae 29119*	'almost everywhere' relation for two functions F and G with regard to the measure M. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- dom R = D   &    |- ( ph -> R e. _V )   &    |- ( ph -> M e. U. ran measures )   &    |- ( ph -> F e. ( D ^m U. dom M ) )   &    |- ( ph -> G e. ( D ^m U. dom M ) )   =>    |- ( ph -> ( F ( R~ a.e. M ) G <-> { x e. U. dom M | ( F ` x ) R ( G ` x ) }a.e. M ) )
21.3.15.11  Measurable functions
Syntax	cmbfm 29120	Extend class notation with the measurable functions builder.
class MblFnM
Definition	df-mbfm 29121*	Define the measurable function builder, which generates the set of measurable functions from a measurable space to another one. Here, the measurable spaces are given using their sigma-algebras s and t, and the spaces themselves are recovered by U. s and U. t. Note the similarities between the definition of measurable functions in measure theory, and of continuous functions in topology. This is the definition for the generic measure theory. For the specific case of functions from RR to CC, see df-mbf 22625. (Contributed by Thierry Arnoux, 23-Jan-2017.)
|- MblFnM = ( s e. U. ran sigAlgebra , t e. U. ran sigAlgebra |-> { f e. ( U. t ^m U. s ) | A. x e. t ( `' f " x ) e. s } )
Theorem	ismbfm 29122*	The predicate " F is a measurable function from the measurable space S to the measurable space T". Cf. ismbf 22634. (Contributed by Thierry Arnoux, 23-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   =>    |- ( ph -> ( F e. ( SMblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )
Theorem	elunirnmbfm 29123*	The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017.)
|- ( F e. U. ran MblFnM <-> E. s e. U. ran sigAlgebra E. t e. U. ran sigAlgebra ( F e. ( U. t ^m U. s ) /\ A. x e. t ( `' F " x ) e. s ) )
Theorem	mbfmfun 29124	A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017.)
|- ( ph -> F e. U. ran MblFnM )   =>    |- ( ph -> Fun F )
Theorem	mbfmf 29125	A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   &    |- ( ph -> F e. ( SMblFnM T ) )   =>    |- ( ph -> F : U. S --> U. T )
Theorem	isanmbfm 29126	The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   &    |- ( ph -> F e. ( SMblFnM T ) )   =>    |- ( ph -> F e. U. ran MblFnM )
Theorem	mbfmcnvima 29127	The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   &    |- ( ph -> F e. ( SMblFnM T ) )   &    |- ( ph -> A e. T )   =>    |- ( ph -> ( `' F " A ) e. S )
Theorem	mbfmbfm 29128	A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017.)
|- ( ph -> M e. U. ran measures )   &    |- ( ph -> J e. Top )   &    |- ( ph -> F e. ( dom MMblFnM (sigaGen ` J ) ) )   =>    |- ( ph -> F e. U. ran MblFnM )
Theorem	mbfmcst 29129*	A constant function is measurable. Cf. mbfconst 22639. (Contributed by Thierry Arnoux, 26-Jan-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   &    |- ( ph -> F = ( x e. U. S |-> A ) )   &    |- ( ph -> A e. U. T )   =>    |- ( ph -> F e. ( SMblFnM T ) )
Theorem	1stmbfm 29130	The first projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   =>    |- ( ph -> ( 1st |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM S ) )
Theorem	2ndmbfm 29131	The second projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   =>    |- ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM T ) )
Theorem	imambfm 29132*	If the sigma-algebra in the range of a given function is generated by a collection of basic sets K, then to check the measurability of that function, we need only consider inverse images of basic sets a. (Contributed by Thierry Arnoux, 4-Jun-2017.)
|- ( ph -> K e. _V )   &    |- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T = (sigaGen ` K ) )   =>    |- ( ph -> ( F e. ( SMblFnM T ) <-> ( F : U. S --> U. T /\ A. a e. K ( `' F " a ) e. S ) ) )
Theorem	cnmbfm 29133	A continuous function is measurable with respect to the Borel Algebra of its domain and range. (Contributed by Thierry Arnoux, 3-Jun-2017.)
|- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> S = (sigaGen ` J ) )   &    |- ( ph -> T = (sigaGen ` K ) )   =>    |- ( ph -> F e. ( SMblFnM T ) )
Theorem	mbfmco 29134	The composition of two measurable functions is measurable. ( cf. cnmpt11 20726) (Contributed by Thierry Arnoux, 4-Jun-2017.)
|- ( ph -> R e. U. ran sigAlgebra )   &    |- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   &    |- ( ph -> F e. ( RMblFnM S ) )   &    |- ( ph -> G e. ( SMblFnM T ) )   =>    |- ( ph -> ( G o. F ) e. ( RMblFnM T ) )
Theorem	mbfmco2 29135*	The pair building of two measurable functions is measurable. ( cf. cnmpt1t 20728). (Contributed by Thierry Arnoux, 6-Jun-2017.)
|- ( ph -> R e. U. ran sigAlgebra )   &    |- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> T e. U. ran sigAlgebra )   &    |- ( ph -> F e. ( RMblFnM S ) )   &    |- ( ph -> G e. ( RMblFnM T ) )   &    |- H = ( x e. U. R |-> <. ( F ` x ) , ( G ` x ) >. )   =>    |- ( ph -> H e. ( RMblFnM ( S ×s T ) ) )
Theorem	mbfmvolf 29136	Measurable functions with respect to the Lebesgue measure are real-valued functions on the real numbers. (Contributed by Thierry Arnoux, 27-Mar-2017.)
|- ( F e. ( dom volMblFnM𝔅ℝ ) -> F : RR --> RR )
Theorem	elmbfmvol2 29137	Measurable functions with respect to the Lebesgue measure. We only have the inclusion, since MblFn includes complex-valued functions. (Contributed by Thierry Arnoux, 26-Jan-2017.)
|- ( F e. ( dom volMblFnM𝔅ℝ ) -> F e. MblFn )
Theorem	mbfmcnt 29138	All functions are measurable with respect to the counting measure. (Contributed by Thierry Arnoux, 24-Jan-2017.)
|- ( O e. V -> ( ~P OMblFnM𝔅ℝ ) = ( RR ^m O ) )
21.3.15.12  Borel Algebra on ` ( RR X. RR ) `
Theorem	br2base 29139*	The base set for the generator of the Borel sigma-algebra on ( RR X. RR ) is indeed ( RR X. RR ). (Contributed by Thierry Arnoux, 22-Sep-2017.)
|- U. ran ( x e. 𝔅ℝ , y e. 𝔅ℝ |-> ( x X. y ) ) = ( RR X. RR )
Theorem	dya2ub 29140	An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017.)
|- ( R e. RR+ -> ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R )
Theorem	sxbrsigalem0 29141*	The closed half-spaces of ( RR X. RR ) cover ( RR X. RR ). (Contributed by Thierry Arnoux, 11-Oct-2017.)
|- U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR )
Theorem	sxbrsigalem3 29142*	The sigma-algebra generated by the closed half-spaces of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed sets of ( RR X. RR ). (Contributed by Thierry Arnoux, 11-Oct-2017.)
|- J = ( topGen ` ran (,) )   =>    |- (sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) C_ (sigaGen ` ( Clsd ` ( J tX J ) ) )
Theorem	dya2iocival 29143*	The function I returns closed-below open-above dyadic rational intervals covering the real line. This is the same construction as in dyadmbl 22606. (Contributed by Thierry Arnoux, 24-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   =>    |- ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )
Theorem	dya2iocress 29144*	Dyadic intervals are subsets of RR. (Contributed by Thierry Arnoux, 18-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   =>    |- ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) C_ RR )
Theorem	dya2iocbrsiga 29145*	Dyadic intervals are Borel sets of RR. (Contributed by Thierry Arnoux, 22-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   =>    |- ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) e. 𝔅ℝ )
Theorem	dya2icobrsiga 29146*	Dyadic intervals are Borel sets of RR. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 13-Oct-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   =>    |- ran I C_ 𝔅ℝ
Theorem	dya2icoseg 29147*	For any point and any closed-below, open-above interval of RR centered on that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 19-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- N = ( |_ ` ( 1 - ( 2 logb D ) ) )   =>    |- ( ( X e. RR /\ D e. RR+ ) -> E. b e. ran I ( X e. b /\ b C_ ( ( X - D ) (,) ( X + D ) ) ) )
Theorem	dya2icoseg2 29148*	For any point and any open interval of RR containing that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 12-Oct-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   =>    |- ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E. b e. ran I ( X e. b /\ b C_ E ) )
Theorem	dya2iocrfn 29149*	The function returning dyadic square covering for a given size has domain ( ran I X. ran I ). (Contributed by Thierry Arnoux, 19-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- R Fn ( ran I X. ran I )
Theorem	dya2iocct 29150*	The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017.) (Revised by Thierry Arnoux, 11-Oct-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- ran R ~<_ om
Theorem	dya2iocnrect 29151*	For any point of an open rectangle in ( RR X. RR ), there is a closed-below open-above dyadic rational square which contains that point and is included in the rectangle. (Contributed by Thierry Arnoux, 12-Oct-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   &    |- B = ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) )   =>    |- ( ( X e. ( RR X. RR ) /\ A e. B /\ X e. A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
Theorem	dya2iocnei 29152*	For any point of an open set of the usual topology on ( RR X. RR ) there is a closed-below open-above dyadic rational square which contains that point and is entirely in the open set. (Contributed by Thierry Arnoux, 21-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- ( ( A e. ( J tX J ) /\ X e. A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
Theorem	dya2iocuni 29153*	Every open set of ( RR X. RR ) is a union of closed-below open-above dyadic rational rectangular subsets of ( RR X. RR ). This union must be a countable union by dya2iocct 29150. (Contributed by Thierry Arnoux, 18-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- ( A e. ( J tX J ) -> E. c e. ~P ran R U. c = A )
Theorem	dya2iocucvr 29154*	The dyadic rectangular set collection covers ( RR X. RR ). (Contributed by Thierry Arnoux, 18-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- U. ran R = ( RR X. RR )
Theorem	sxbrsigalem1 29155*	The Borel algebra on ( RR X. RR ) is a subset of the sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ). This is a step of the proof of Proposition 1.1.5 of [Cohn] p. 4. (Contributed by Thierry Arnoux, 17-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- (sigaGen ` ( J tX J ) ) C_ (sigaGen ` ran R )
Theorem	sxbrsigalem2 29156*	The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed half-spaces of ( RR X. RR ). The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- (sigaGen ` ran R ) C_ (sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) )
Theorem	sxbrsigalem4 29157*	The Borel algebra on ( RR X. RR ) is generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ). Proposition 1.1.5 of [Cohn] p. 4 . Note that the interval used in this formalization are closed-below, open-above instead of open-below, closed-above in the proof as they are ultimately generated by the floor function. (Contributed by Thierry Arnoux, 21-Sep-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- (sigaGen ` ( J tX J ) ) = (sigaGen ` ran R )
Theorem	sxbrsigalem5 29158*	First direction for sxbrsiga 29160. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 11-Oct-2017.)
|- J = ( topGen ` ran (,) )   &    |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )   &    |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )   =>    |- (sigaGen ` ( J tX J ) ) C_ (𝔅ℝ ×s 𝔅ℝ )
Theorem	sxbrsigalem6 29159	First direction for sxbrsiga 29160, same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017.)
|- J = ( topGen ` ran (,) )   =>    |- (sigaGen ` ( J tX J ) ) C_ (𝔅ℝ ×s 𝔅ℝ )
Theorem	sxbrsiga 29160	The product sigma-algebra (𝔅ℝ ×s 𝔅ℝ ) is the Borel algebra on ( RR X. RR ) See example 5.1.1 of [Cohn] p. 143 . (Contributed by Thierry Arnoux, 10-Oct-2017.)
|- J = ( topGen ` ran (,) )   =>    |- (𝔅ℝ ×s 𝔅ℝ ) = (sigaGen ` ( J tX J ) )
21.3.15.13  Caratheodory's extension theorem In this section, we define a function toOMeas which constructs an outer measure, from a pre-measure R. An explicit generic definition of an outer measure is not given. It consists of the three following statements: - the outer measure of an empty set is zero (oms0 29173) - it is monotone (omsmon 29174) - it is countably sub-additive (omssubadd 29176) See Definition 1.11.1 of [Bogachev] p. 41.
Syntax	coms 29161	Class declaration for the outer measure construction function.
class toOMeas
Syntax	comsold 29162	Class declaration for the outer measure construction function (old version).
class toOMeas
Definition	df-oms 29163*	Define a function constructing an outer measure. See omsval 29165 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- toOMeas = ( r e. _V |-> ( a e. ~P U. dom r |-> inf ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , < ) ) )
Definition	df-omsOLD 29164*	Define a function constructing an outer measure. See omsval 29165 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.) Obsolete version of df-oms 29163 as of 4-Oct-2020. (New usage is discouraged.)
|- toOMeas = ( r e. _V |-> ( a e. ~P U. dom r |-> sup ( ran ( x e. { z e. ~P dom r | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( r ` y ) ) , ( 0 [,] +oo ) , `' < ) ) )
Theorem	omsval 29165*	Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- ( R e. _V -> (toOMeas ` R ) = ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) )
Theorem	omsfval 29166*	Value of the outer measure evaluated for a given set A. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( (toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
Theorem	omscl 29167*	A closure lemma for the constructed outer measure. (Contributed by Thierry Arnoux, 17-Sep-2019.)
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
Theorem	omsf 29168	A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
Theorem	omsvalOLD 29169*	Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019.) Obsolete version of omsval 29165 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( R e. _V -> (toOMeas ` R ) = ( a e. ~P U. dom R |-> sup ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , `' < ) ) )
Theorem	omsfvalOLD 29170*	Value of the outer measure evaluated for a given set A. (Contributed by Thierry Arnoux, 15-Sep-2019.) Obsolete version of omsfval 29166 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( (toOMeas ` R ) ` A ) = sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , `' < ) )
Theorem	omsclOLD 29171*	A closure lemma for the constructed outer measure. (Contributed by Thierry Arnoux, 17-Sep-2019.) Obsolete version of omscl 29167 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
Theorem	omsfOLD 29172	A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019.) Obsolete version of omsf 29168 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
Theorem	oms0 29173	A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> (/) e. dom R )   &    |- ( ph -> ( R ` (/) ) = 0 )   =>    |- ( ph -> ( M ` (/) ) = 0 )
Theorem	omsmon 29174	A constructed outer measure is monotone. Note in Example 1.5.2 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> B C_ U. Q )   =>    |- ( ph -> ( M ` A ) <_ ( M ` B ) )
Theorem	omssubaddlem 29175*	For any small margin E, we can find a covering approaching the outer measure of a set A by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ U. Q )   &    |- ( ph -> ( M ` A ) e. RR )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + E ) )
Theorem	omssubadd 29176*	A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) (Revised by AV, 4-Oct-2020.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ( ph /\ y e. X ) -> A C_ U. Q )   &    |- ( ph -> X ~<_ om )   =>    |- ( ph -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )
Theorem	oms0OLD 29177	A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019.) Obsolete version of oms0 29173 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> (/) e. dom R )   &    |- ( ph -> ( R ` (/) ) = 0 )   =>    |- ( ph -> ( M ` (/) ) = 0 )
Theorem	omsmonOLD 29178	A constructed outer measure is monotone. Note in Example 1.5.2 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019.) Obsolete version of omsmon 29174 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> B C_ U. Q )   =>    |- ( ph -> ( M ` A ) <_ ( M ` B ) )
Theorem	omssubaddlemOLD 29179*	For any small margin E, we can find a covering approaching the outer measure of a set A by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019.) Obsolete version of omssubaddlem 29175 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ U. Q )   &    |- ( ph -> ( M ` A ) e. RR )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + E ) )
Theorem	omssubaddOLD 29180*	A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) Obsolete version of omssubadd 29176 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- M = (toOMeas ` R )   &    |- ( ph -> Q e. V )   &    |- ( ph -> R : Q --> ( 0 [,] +oo ) )   &    |- ( ( ph /\ y e. X ) -> A C_ U. Q )   &    |- ( ph -> X ~<_ om )   =>    |- ( ph -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )
Syntax	ccarsg 29181	Class declaration for the Caratheodory sigma-Algebra construction.
class toCaraSiga
Definition	df-carsg 29182*	Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 29183 for its value. Definition 1.11.2 of [Bogachev] p. 41. (Contributed by Thierry Arnoux, 17-May-2020.)
|- toCaraSiga = ( m e. _V |-> { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) } )
Theorem	carsgval 29183*	Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   =>    |- ( ph -> (toCaraSiga ` M ) = { a e. ~P O | A. e e. ~P O ( ( M ` ( e i^i a ) ) +e ( M ` ( e \ a ) ) ) = ( M ` e ) } )
Theorem	carsgcl 29184	Closure of the Caratheodory measurable sets. (Contributed by Thierry Arnoux, 17-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   =>    |- ( ph -> (toCaraSiga ` M ) C_ ~P O )
Theorem	elcarsg 29185*	Property of being a Catatheodory measurable set. (Contributed by Thierry Arnoux, 17-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   =>    |- ( ph -> ( A e. (toCaraSiga ` M ) <-> ( A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) ) ) )
Theorem	baselcarsg 29186	The universe set, O, is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   =>    |- ( ph -> O e. (toCaraSiga ` M ) )
Theorem	0elcarsg 29187	The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   =>    |- ( ph -> (/) e. (toCaraSiga ` M ) )
Theorem	carsguni 29188	The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   =>    |- ( ph -> U. (toCaraSiga ` M ) = O )
Theorem	elcarsgss 29189	Caratheodory measurable sets are subsets of the universe. (Contributed by Thierry Arnoux, 21-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. (toCaraSiga ` M ) )   =>    |- ( ph -> A C_ O )
Theorem	difelcarsg 29190	The Caratheodory measurable sets are closed under complement. (Contributed by Thierry Arnoux, 17-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. (toCaraSiga ` M ) )   =>    |- ( ph -> ( O \ A ) e. (toCaraSiga ` M ) )
Theorem	inelcarsg 29191*	The Caratheodory measurable sets are closed under intersection. (Contributed by Thierry Arnoux, 18-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. (toCaraSiga ` M ) )   &    |- ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )   &    |- ( ph -> B e. (toCaraSiga ` M ) )   =>    |- ( ph -> ( A i^i B ) e. (toCaraSiga ` M ) )
Theorem	unelcarsg 29192*	The Caratheodory-measurable sets are closed under pairwise unions. (Contributed by Thierry Arnoux, 21-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. (toCaraSiga ` M ) )   &    |- ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )   &    |- ( ph -> B e. (toCaraSiga ` M ) )   =>    |- ( ph -> ( A u. B ) e. (toCaraSiga ` M ) )
Theorem	difelcarsg2 29193*	The Caratheodory-measurable sets are closed under class difference. (Contributed by Thierry Arnoux, 30-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. (toCaraSiga ` M ) )   &    |- ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )   &    |- ( ph -> B e. (toCaraSiga ` M ) )   =>    |- ( ph -> ( A \ B ) e. (toCaraSiga ` M ) )
Theorem	carsgmon 29194*	Utility lemma: Apply monotony. (Contributed by Thierry Arnoux, 29-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> B e. ~P O )   &    |- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )   =>    |- ( ph -> ( M ` A ) <_ ( M ` B ) )
Theorem	carsgsigalem 29195*	Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   &    |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )   =>    |- ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )
Theorem	fiunelcarsg 29196*	The Caratheodory measurable sets are closed under finite union. (Contributed by Thierry Arnoux, 23-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   &    |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ (toCaraSiga ` M ) )   =>    |- ( ph -> U. A e. (toCaraSiga ` M ) )
Theorem	carsgclctunlem1 29197*	Lemma for carsgclctun 29201. (Contributed by Thierry Arnoux, 23-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   &    |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ (toCaraSiga ` M ) )   &    |- ( ph -> Disj y e. A y )   &    |- ( ph -> E e. ~P O )   =>    |- ( ph -> ( M ` ( E i^i U. A ) ) = Σ* y e. A ( M ` ( E i^i y ) ) )
Theorem	carsggect 29198*	The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   &    |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )   &    |- ( ph -> -. (/) e. A )   &    |- ( ph -> A ~<_ om )   &    |- ( ph -> A C_ (toCaraSiga ` M ) )   &    |- ( ph -> Disj y e. A y )   &    |- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )   =>    |- ( ph -> Σ* z e. A ( M ` z ) <_ ( M ` U. A ) )
Theorem	carsgclctunlem2 29199*	Lemma for carsgclctun 29201. (Contributed by Thierry Arnoux, 25-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   &    |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )   &    |- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )   &    |- ( ph -> Disj k e. NN A )   &    |- ( ( ph /\ k e. NN ) -> A e. (toCaraSiga ` M ) )   &    |- ( ph -> E e. ~P O )   &    |- ( ph -> ( M ` E ) =/= +oo )   =>    |- ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( M ` E ) )
Theorem	carsgclctunlem3 29200*	Lemma for carsgclctun 29201. (Contributed by Thierry Arnoux, 24-May-2020.)
|- ( ph -> O e. V )   &    |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )   &    |- ( ph -> ( M ` (/) ) = 0 )   &    |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )   &    |- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )   &    |- ( ph -> A ~<_ om )   &    |- ( ph -> A C_ (toCaraSiga ` M ) )   &    |- ( ph -> E e. ~P O )   =>    |- ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )