P. 406 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40501-40600   *Has distinct variable group(s)

Type	Label	Description
Statement
20.32.18  n-dimensional Euclidean space
Theorem	rrxtopn 40501*	The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. V )   =>    |- ( ph -> ( TopOpen ` (ℝ^ ` I ) ) = ( MetOpen ` ( f e. ( Base ` (ℝ^ ` I ) ) , g e. ( Base ` (ℝ^ ` I ) ) |-> ( sqr ` (RRfld gsumg ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) ) )
Theorem	rrxngp 40502	Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( I e. V -> (ℝ^ ` I ) e. NrmGrp )
Theorem	rrxbasefi 40503	The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of ( RR ^m X ) for the development of the Lebeasgue measure theory for n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   &    |- H = (ℝ^ ` X )   &    |- B = ( Base ` H )   =>    |- ( ph -> B = ( RR ^m X ) )
Theorem	rrxtps 40504	Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( I e. V -> (ℝ^ ` I ) e. TopSp )
Theorem	rrxdsfi 40505*	The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- H = (ℝ^ ` I )   &    |- B = ( RR ^m I )   =>    |- ( I e. Fin -> ( dist ` H ) = ( f e. B , g e. B |-> ( sqr ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
Theorem	rrxtopnfi 40506*	The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   =>    |- ( ph -> ( TopOpen ` (ℝ^ ` I ) ) = ( MetOpen ` ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqr ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )
Theorem	rrxmetfi 40507	Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- D = ( dist ` (ℝ^ ` I ) )   =>    |- ( I e. Fin -> D e. ( Met ` ( RR ^m I ) ) )
Theorem	rrxtopon 40508	The topology on Generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- J = ( TopOpen ` (ℝ^ ` I ) )   =>    |- ( I e. V -> J e. (TopOn ` ( Base ` (ℝ^ ` I ) ) ) )
Theorem	rrxtop 40509	The topology on Generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- J = ( TopOpen ` (ℝ^ ` I ) )   =>    |- ( I e. V -> J e. Top )
Theorem	rrndistlt 40510*	Given two points in the space of n-dimensional real numbers, if every component is closer than E then the distance between the two points is less then ( ( sqr ` n ) x. E ) (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   &    |- ( ph -> I =/= (/) )   &    |- N = ( # ` I )   &    |- ( ph -> X e. ( RR ^m I ) )   &    |- ( ph -> Y e. ( RR ^m I ) )   &    |- ( ( ph /\ i e. I ) -> ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) < E )   &    |- ( ph -> E e. RR+ )   &    |- D = ( dist ` (ℝ^ ` I ) )   =>    |- ( ph -> ( X D Y ) < ( ( sqr ` N ) x. E ) )
Theorem	rrxtoponfi 40511	The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- J = ( TopOpen ` (ℝ^ ` I ) )   =>    |- ( I e. Fin -> J e. (TopOn ` ( RR ^m I ) ) )
Theorem	rrxunitopnfi 40512	The base set of the standard topology on the space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( X e. Fin -> U. ( TopOpen ` (ℝ^ ` X ) ) = ( RR ^m X ) )
Theorem	rrxtopn0 40513	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( TopOpen ` (ℝ^ ` (/) ) ) = ~P { (/) }
Theorem	qndenserrnbllem 40514*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   &    |- ( ph -> I =/= (/) )   &    |- ( ph -> X e. ( RR ^m I ) )   &    |- D = ( dist ` (ℝ^ ` I ) )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )
Theorem	qndenserrnbl 40515*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   &    |- ( ph -> X e. ( RR ^m I ) )   &    |- D = ( dist ` (ℝ^ ` I ) )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. y e. ( QQ ^m I ) y e. ( X ( ball ` D ) E ) )
Theorem	rrxtopn0b 40516	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( TopOpen ` (ℝ^ ` (/) ) ) = { (/) , { (/) } }
Theorem	qndenserrnopnlem 40517*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   &    |- J = ( TopOpen ` (ℝ^ ` I ) )   &    |- ( ph -> V e. J )   &    |- ( ph -> X e. V )   &    |- D = ( dist ` (ℝ^ ` I ) )   =>    |- ( ph -> E. y e. ( QQ ^m I ) y e. V )
Theorem	qndenserrnopn 40518*	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   &    |- J = ( TopOpen ` (ℝ^ ` I ) )   &    |- ( ph -> V e. J )   &    |- ( ph -> V =/= (/) )   =>    |- ( ph -> E. y e. ( QQ ^m I ) y e. V )
Theorem	qndenserrn 40519	n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I e. Fin )   &    |- J = ( TopOpen ` (ℝ^ ` I ) )   =>    |- ( ph -> ( ( cls ` J ) ` ( QQ ^m I ) ) = ( RR ^m I ) )
Theorem	rrxsnicc 40520*	A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. ( RR ^m X ) )   =>    |- ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = { A } )
Theorem	rrnprjdstle 40521	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- ( ph -> F : X --> RR )   &    |- ( ph -> G : X --> RR )   &    |- ( ph -> I e. X )   &    |- D = ( dist ` (ℝ^ ` X ) )   =>    |- ( ph -> ( abs ` ( ( F ` I ) - ( G ` I ) ) ) <_ ( F D G ) )
Theorem	rrndsmet 40522*	D is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqr ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )   =>    |- ( ph -> D e. ( Met ` ( RR ^m X ) ) )
Theorem	rrndsxmet 40523*	D is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqr ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )   =>    |- ( ph -> D e. ( *Met ` ( RR ^m X ) ) )
Theorem	ioorrnopnlem 40524*	The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )   &    |- H = ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )   &    |- E = inf ( H , RR , < )   &    |- V = ( F ( ball ` D ) E )   &    |- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqr ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )   =>    |- ( ph -> E. v e. ( TopOpen ` (ℝ^ ` X ) ) ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
Theorem	ioorrnopn 40525*	The indexed product of open intervals is an open set in (ℝ^ ` X ). (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` (ℝ^ ` X ) ) )
Theorem	ioorrnopnxrlem 40526*	Given a point F that belongs to an indexed product of (possibly unbounded) open intervals, then F belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR* )   &    |- ( ph -> B : X --> RR* )   &    |- ( ph -> F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )   &    |- L = ( i e. X |-> if ( ( A ` i ) = -oo , ( ( F ` i ) - 1 ) , ( A ` i ) ) )   &    |- R = ( i e. X |-> if ( ( B ` i ) = +oo , ( ( F ` i ) + 1 ) , ( B ` i ) ) )   &    |- V = X_ i e. X ( ( L ` i ) (,) ( R ` i ) )   =>    |- ( ph -> E. v e. ( TopOpen ` (ℝ^ ` X ) ) ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
Theorem	ioorrnopnxr 40527*	The indexed product of open intervals is an open set in (ℝ^ ` X ). Similar to ioorrnopn 40525 but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR* )   &    |- ( ph -> B : X --> RR* )   =>    |- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` (ℝ^ ` X ) ) )
20.32.19  Basic measure theory
20.32.19.1  σ-Algebras Proofs for most of the theorems in section 111 of [Fremlin1]
Syntax	csalg 40528	Extend class notation with the class of all sigma-algebras.
class SAlg
Definition	df-salg 40529*	Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- SAlg = { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ om -> U. y e. x ) ) }
Syntax	csalon 40530	Extend class notation with the class of sigma-algebras on a set.
class SalOn
Definition	df-salon 40531*	Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- SalOn = ( x e. _V |-> { s e. SAlg | U. s = x } )
Syntax	csalgen 40532	Extend class notation with the class of sigma-algebra generator.
class SalGen
Definition	df-salgen 40533*	Define the sigma-algebra generated by a given set. Definition 111G (b) of [Fremlin1] p. 13. The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set, see dfsalgen2 40559. The base set of the sigma-algebras used for the intersection needs to be the same, otherwise the resulting set is not guaranteed to be a sigma-algebra, as shown in the counterexample salgencntex 40561. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.)
|- SalGen = ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )
Theorem	issal 40534*	Express the predicate " S is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( S e. V -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ om -> U. y e. S ) ) ) )
Theorem	pwsal 40535	The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( X e. V -> ~P X e. SAlg )
Theorem	salunicl 40536	SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> T e. ~P S )   &    |- ( ph -> T ~<_ om )   =>    |- ( ph -> U. T e. S )
Theorem	saluncl 40537	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E u. F ) e. S )
Theorem	prsal 40538	The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( X e. V -> { (/) , X } e. SAlg )
Theorem	saldifcl 40539	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )
Theorem	0sal 40540	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( S e. SAlg -> (/) e. S )
Theorem	salgenval 40541*	The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( X e. V -> (SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
Theorem	saliuncl 40542*	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> K ~<_ om )   &    |- ( ( ph /\ k e. K ) -> E e. S )   =>    |- ( ph -> U_ k e. K E e. S )
Theorem	salincl 40543	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i F ) e. S )
Theorem	saluni 40544	A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( S e. SAlg -> U. S e. S )
Theorem	saliincl 40545*	SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> K ~<_ om )   &    |- ( ph -> K =/= (/) )   &    |- ( ( ph /\ k e. K ) -> E e. S )   =>    |- ( ph -> |^|_ k e. K E e. S )
Theorem	saldifcl2 40546	The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E \ F ) e. S )
Theorem	intsaluni 40547*	The union of an arbitrary intersection of sigma-algebras on the same set X, is X. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> G C_ SAlg )   &    |- ( ph -> G =/= (/) )   &    |- ( ( ph /\ s e. G ) -> U. s = X )   =>    |- ( ph -> U. |^| G = X )
Theorem	intsal 40548*	The arbitrary intersection of sigma-algebra (on the same set X) is a sigma-algebra ( on the same set X, see intsaluni 40547). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> G C_ SAlg )   &    |- ( ph -> G =/= (/) )   &    |- ( ( ph /\ s e. G ) -> U. s = X )   =>    |- ( ph -> |^| G e. SAlg )
Theorem	salgenn0 40549*	The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )
Theorem	salgencl 40550	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( X e. V -> (SalGen ` X ) e. SAlg )
Theorem	issald 40551*	Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> S e. V )   &    |- ( ph -> (/) e. S )   &    |- X = U. S   &    |- ( ( ph /\ y e. S ) -> ( X \ y ) e. S )   &    |- ( ( ph /\ y e. ~P S /\ y ~<_ om ) -> U. y e. S )   =>    |- ( ph -> S e. SAlg )
Theorem	salexct 40552*	An example of non trivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. V )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   =>    |- ( ph -> S e. SAlg )
Theorem	sssalgen 40553	A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- S = (SalGen ` X )   =>    |- ( X e. V -> X C_ S )
Theorem	salgenss 40554	The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set. Proposition 111G (b) of [Fremlin1] p. 13. Notice that the condition "on the same base set" is needed, see the counterexample salgensscntex 40562, where a sigma-algebra is shown that includes a set, but does not include the sigma-algebra generated (the key is that its base set is larger than the base set of the generating set). (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> X e. V )   &    |- G = (SalGen ` X )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> X C_ S )   &    |- ( ph -> U. S = U. X )   =>    |- ( ph -> G C_ S )
Theorem	salgenuni 40555	The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> X e. V )   &    |- S = (SalGen ` X )   &    |- U = U. X   =>    |- ( ph -> U. S = U )
Theorem	issalgend 40556*	One side of dfsalgen2 40559. If a sigma-algebra on U. X includes X and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by X. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> X e. V )   &    |- ( ph -> S e. SAlg )   &    |- ( ph -> U. S = U. X )   &    |- ( ph -> X C_ S )   &    |- ( ( ph /\ ( y e. SAlg /\ U. y = U. X /\ X C_ y ) ) -> S C_ y )   =>    |- ( ph -> (SalGen ` X ) = S )
Theorem	salexct2 40557*	An example of a subset that does not belong to a non trivial sigma-algebra, see salexct 40552. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- B = ( 0 [,] 1 )   =>    |- -. B e. S
Theorem	unisalgen 40558	The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> X e. V )   &    |- S = (SalGen ` X )   &    |- U = U. X   =>    |- ( ph -> U e. S )
Theorem	dfsalgen2 40559*	Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> X e. V )   =>    |- ( ph -> ( (SalGen ` X ) = S <-> ( ( S e. SAlg /\ U. S = U. X /\ X C_ S ) /\ A. y e. SAlg ( ( U. y = U. X /\ X C_ y ) -> S C_ y ) ) ) )
Theorem	salexct3 40560*	An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- X = ran ( y e. ( 0 [,] 1 ) |-> { y } )   =>    |- ( S e. SAlg /\ X C_ S /\ -. U. X e. S )
Theorem	salgencntex 40561*	This counterexample shows that df-salgen 40533 needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- B = ( 0 [,] 1 )   &    |- T = ~P B   &    |- C = ( S i^i T )   &    |- Z = |^| { s e. SAlg | C C_ s }   =>    |- -. Z e. SAlg
Theorem	salgensscntex 40562*	This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- X = ran ( y e. ( 0 [,] 1 ) |-> { y } )   &    |- G = (SalGen ` X )   =>    |- ( X C_ S /\ S e. SAlg /\ -. G C_ S )
Theorem	issalnnd 40563*	Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> S e. V )   &    |- ( ph -> (/) e. S )   &    |- X = U. S   &    |- ( ( ph /\ y e. S ) -> ( X \ y ) e. S )   &    |- ( ( ph /\ e : NN --> S ) -> U_ n e. NN ( e ` n ) e. S )   =>    |- ( ph -> S e. SAlg )
Theorem	dmvolsal 40564	Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- dom vol e. SAlg
Theorem	saldifcld 40565	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> E e. S )   =>    |- ( ph -> ( U. S \ E ) e. S )
Theorem	saluncld 40566	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> E e. S )   &    |- ( ph -> F e. S )   =>    |- ( ph -> ( E u. F ) e. S )
Theorem	salgencld 40567	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> X e. V )   &    |- S = (SalGen ` X )   =>    |- ( ph -> S e. SAlg )
Theorem	0sald 40568	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   =>    |- ( ph -> (/) e. S )
Theorem	iooborel 40569	An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   =>    |- ( A (,) C ) e. B
Theorem	salincld 40570	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> E e. S )   &    |- ( ph -> F e. S )   =>    |- ( ph -> ( E i^i F ) e. S )
Theorem	salunid 40571	A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   =>    |- ( ph -> U. S e. S )
Theorem	unisalgen2 40572	The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   &    |- S = (SalGen ` A )   =>    |- ( ph -> U. S = U. A )
Theorem	bor1sal 40573	The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   =>    |- B e. SAlg
Theorem	iocborel 40574	A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> C e. RR )   &    |- J = ( topGen ` ran (,) )   &    |- B = (SalGen ` J )   =>    |- ( ph -> ( A (,] C ) e. B )
Theorem	subsaliuncllem 40575*	A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ y ph   &    |- ( ph -> S e. V )   &    |- G = ( n e. NN |-> { x e. S | ( F ` n ) = ( x i^i D ) } )   &    |- E = ( H o. G )   &    |- ( ph -> H Fn ran G )   &    |- ( ph -> A. y e. ran G ( H ` y ) e. y )   =>    |- ( ph -> E. e e. ( S ^m NN ) A. n e. NN ( F ` n ) = ( ( e ` n ) i^i D ) )
Theorem	subsaliuncl 40576*	A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> D e. V )   &    |- T = ( S ↾t D )   &    |- ( ph -> F : NN --> T )   =>    |- ( ph -> U_ n e. NN ( F ` n ) e. T )
Theorem	subsalsal 40577	A subspace sigma-algebra is a sigma algebra. This is Lemma 121A of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> D e. V )   &    |- T = ( S ↾t D )   =>    |- ( ph -> T e. SAlg )
Theorem	subsaluni 40578	A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> S e. SAlg )   &    |- ( ph -> A C_ U. S )   =>    |- ( ph -> A e. ( S ↾t A ) )
20.32.19.2  Sum of nonnegative extended reals
Syntax	csumge0 40579	Extend class notation to include the sum of nonnegative extended reals.
class Σ^
Definition	df-sumge0 40580*	Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.
|- Σ^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )
Theorem	sge0rnre 40581*	When Σ^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
Theorem	fge0icoicc 40582	If F maps to nonnegative reals, then F maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> F : X --> ( 0 [,] +oo ) )
Theorem	sge0val 40583*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> (Σ^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) ) )
Theorem	fge0npnf 40584	If F maps to nonnegative reals, then +oo is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> -. +oo e. ran F )
Theorem	sge0rnn0 40585*	The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/)
Theorem	sge0vald 40586*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) )
Theorem	fge0iccico 40587	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> -. +oo e. ran F )   =>    |- ( ph -> F : X --> ( 0 [,) +oo ) )
Theorem	gsumge0cl 40588	Closure of group sum, for finitely supported nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> F finSupp 0 )   =>    |- ( ph -> ( G gsumg F ) e. ( 0 [,] +oo ) )
Theorem	sge0reval 40589*	Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
Theorem	sge0pnfval 40590	If a term in the sum of nonnegative extended reals is +oo, then the value of the sum is +oo. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> +oo e. ran F )   =>    |- ( ph -> (Σ^ ` F ) = +oo )
Theorem	fge0iccre 40591	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> -. +oo e. ran F )   =>    |- ( ph -> F : X --> RR )
Theorem	sge0z 40592*	Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> 0 ) ) = 0 )
Theorem	sge00 40593	The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- (Σ^ ` (/) ) = 0
Theorem	fsumlesge0 40594*	Every finite subsum of nonnegative reals is less than or equal to the extended sum over the whole (possibly infinite) domain. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,) +oo ) )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Y e. Fin )   =>    |- ( ph -> sum_ x e. Y ( F ` x ) <_ (Σ^ ` F ) )
Theorem	sge0revalmpt 40595*	Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) , RR* , < ) )
Theorem	sge0sn 40596	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : { A } --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = ( F ` A ) )
Theorem	sge0tsms 40597	Σ^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) e. ( G tsums F ) )
Theorem	sge0cl 40598	The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) e. ( 0 [,] +oo ) )
Theorem	sge0f1o 40599*	Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- F/ n ph   &    |- ( k = G -> B = D )   &    |- ( ph -> C e. V )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = (Σ^ ` ( n e. C |-> D ) ) )
Theorem	sge0snmpt 40600*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> C e. ( 0 [,] +oo ) )   &    |- ( k = A -> B = C )   =>    |- ( ph -> (Σ^ ` ( k e. { A } |-> B ) ) = C )