P. 385 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38401-38500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	omeunle 38401	The outer measure of the union of two sets is less or equal to the sum of the measures, Remark 113B (c) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- ( ph -> A C_ X )   &    |- ( ph -> B C_ X )   =>    |- ( ph -> ( O ` ( A u. B ) ) <_ ( ( O ` A ) +e ( O ` B ) ) )
Theorem	omeiunle 38402*	The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ n ph   &    |- F/_ n E   &    |- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- Z = ( ZZ>= ` N )   &    |- ( ph -> E : Z --> ~P X )   =>    |- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ (Σ^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
Theorem	omelesplit 38403	The outer measure of a set A is less than or equal to the extended addition of the outer measures of the decomposition induced on A by any E. Step (a) in the proof of Caratheodory's Method, Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- ( ph -> A C_ X )   =>    |- ( ph -> ( O ` A ) <_ ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) )
Theorem	omeiunltfirp 38404*	If the outer measure of a countable union is not +oo, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- Z = ( ZZ>= ` N )   &    |- ( ph -> E : Z --> ~P X )   &    |- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. RR )   &    |- ( ph -> Y e. RR+ )   =>    |- ( ph -> E. z e. ( ~P Z i^i Fin ) ( O ` U_ n e. Z ( E ` n ) ) < ( sum_ n e. z ( O ` ( E ` n ) ) + Y ) )
Theorem	omeiunlempt 38405*	The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ n ph   &    |- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- Z = ( ZZ>= ` N )   &    |- ( ( ph /\ n e. Z ) -> E C_ X )   =>    |- ( ph -> ( O ` U_ n e. Z E ) <_ (Σ^ ` ( n e. Z |-> ( O ` E ) ) ) )
Theorem	carageniuncllem1 38406*	The outer measure of A i^i ( G ` n ) is the sum of the outer measures of A i^i ( F ` m ). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   &    |- X = U. dom O   &    |- ( ph -> A C_ X )   &    |- ( ph -> ( O ` A ) e. RR )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> E : Z --> S )   &    |- G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )   &    |- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M..^ n ) ( E ` i ) ) )   &    |- ( ph -> K e. Z )   =>    |- ( ph -> sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) )
Theorem	carageniuncllem2 38407*	The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   &    |- X = U. dom O   &    |- ( ph -> A C_ X )   &    |- ( ph -> ( O ` A ) e. RR )   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> E : Z --> S )   &    |- ( ph -> Y e. RR+ )   &    |- G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )   &    |- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M..^ n ) ( E ` i ) ) )   =>    |- ( ph -> ( ( O ` ( A i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( A \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` A ) + Y ) )
Theorem	carageniuncl 38408*	The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> E : Z --> S )   =>    |- ( ph -> U_ n e. Z ( E ` n ) e. S )
Theorem	caragenunicl 38409	The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   &    |- ( ph -> X C_ S )   &    |- ( ph -> X ~<_ om )   =>    |- ( ph -> U. X e. S )
Theorem	caragensal 38410	Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   =>    |- ( ph -> S e. SAlg )
Theorem	caratheodorylem1 38411*	Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> E : Z --> S )   &    |- ( ph -> Disj n e. Z ( E ` n ) )   &    |- G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( O ` ( G ` N ) ) = (Σ^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) )
Theorem	caratheodorylem2 38412*	Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- S = (CaraGen ` O )   &    |- ( ph -> E : NN --> S )   &    |- ( ph -> Disj n e. NN ( E ` n ) )   &    |- G = ( k e. NN |-> U_ n e. ( 1 ... k ) ( E ` n ) )   =>    |- ( ph -> ( O ` U_ n e. NN ( E ` n ) ) = (Σ^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) )
Theorem	caratheodory 38413	Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> O e. OutMeas )   &    |- S = (CaraGen ` O )   =>    |- ( ph -> ( O |` S ) e. Meas )
Theorem	0ome 38414*	The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. V )   &    |- O = ( x e. ~P X |-> 0 )   =>    |- ( ph -> O e. OutMeas )
Theorem	isomenndlem 38415*	O is sub-additive w.r.t. countable indexed union, implies that O is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> O : ~P X --> ( 0 [,] +oo ) )   &    |- ( ph -> ( O ` (/) ) = 0 )   &    |- ( ph -> Y C_ ~P X )   &    |- ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ (Σ^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )   &    |- ( ph -> B C_ NN )   &    |- ( ph -> F : B -1-1-onto-> Y )   &    |- A = ( n e. NN |-> if ( n e. B , ( F ` n ) , (/) ) )   =>    |- ( ph -> ( O ` U. Y ) <_ (Σ^ ` ( O |` Y ) ) )
Theorem	isomennd 38416*	Sufficient condition to prove that O is an outer measure. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> O : ~P X --> ( 0 [,] +oo ) )   &    |- ( ph -> ( O ` (/) ) = 0 )   &    |- ( ( ph /\ x C_ X /\ y C_ x ) -> ( O ` y ) <_ ( O ` x ) )   &    |- ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ (Σ^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )   =>    |- ( ph -> O e. OutMeas )
Theorem	caragenel2d 38417*	Membership in the Caratheodory's construction. Similar to carageneld 38387, but here "less then or equal" is used, instead of equality. This is Remark 113D of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- S = (CaraGen ` O )   &    |- ( ph -> E e. ~P X )   &    |- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) <_ ( O ` a ) )   =>    |- ( ph -> E e. S )
Theorem	omege0 38418	If the outer measure of a set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- ( ph -> A C_ X )   =>    |- ( ph -> 0 <_ ( O ` A ) )
Theorem	omess0 38419	If the outer measure of a set is 0, then the outer measure of its subsets is 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- ( ph -> A C_ X )   &    |- ( ph -> ( O ` A ) = 0 )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( O ` B ) = 0 )
Theorem	caragencmpl 38420	A measure built with the Caratheodory's construction is complete. See Definition 112Df of [Fremlin1] p. 19. This is Exercise 113Xa of [Fremlin1] p. 21 (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> O e. OutMeas )   &    |- X = U. dom O   &    |- ( ph -> E C_ X )   &    |- ( ph -> ( O ` E ) = 0 )   &    |- S = (CaraGen ` O )   =>    |- ( ph -> E e. S )
21.30.19.5  Lebesgue measure on n-dimensional Real numbers Proof for the most important theorem in section 115 of [Fremlin1] (the plan is to complete the whole section with the next update)
Syntax	covoln 38421	Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers.
class voln*
Definition	df-ovoln 38422*	Define the outer measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- voln* = ( x e. Fin |-> ( y e. ~P ( RR ^m x ) |-> if ( x = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m x ) ^m NN ) ( y C_ U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) ) )
Syntax	cvoln 38423	Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers.
class voln
Definition	df-voln 38424	Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- voln = ( x e. Fin |-> ( (voln* ` x ) |` (CaraGen ` (voln* ` x ) ) ) )
Theorem	vonval 38425	Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> (voln ` X ) = ( (voln* ` X ) |` (CaraGen ` (voln* ` X ) ) ) )
Theorem	ovnval 38426*	Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> (voln* ` X ) = ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) ) )
Theorem	elhoi 38427*	Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. V )   =>    |- ( ph -> ( Y e. ( ( A [,) B ) ^m X ) <-> ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) ) )
Theorem	icoresmbl 38428	A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ran ( [,) |` ( RR X. RR ) ) C_ dom vol
Theorem	hoissre 38429*	The projection of a half-open interval onto a single dimension is a subset of RR. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> I : X --> ( RR X. RR ) )   =>    |- ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) C_ RR )
Theorem	ovnval2 38430*	Value of the Lebesgue outer measure of a subset A of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   =>    |- ( ph -> ( (voln* ` X ) ` A ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )
Theorem	volicorecl 38431	The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR )
Theorem	hoiprodcl 38432*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I : X --> ( RR X. RR ) )   =>    |- ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. ( 0 [,) +oo ) )
Theorem	hoicvr 38433*	I is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- I = ( j e. NN |-> ( x e. X |-> <. -u j , j >. ) )   &    |- ( ph -> X e. Fin )   =>    |- ( ph -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
Theorem	hoissrrn 38434*	A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> I : X --> ( RR X. RR ) )   =>    |- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) C_ ( RR ^m X ) )
Theorem	ovn0val 38435	The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A C_ ( RR ^m (/) ) )   =>    |- ( ph -> ( (voln* ` (/) ) ` A ) = 0 )
Theorem	ovnn0val 38436*	The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   =>    |- ( ph -> ( (voln* ` X ) ` A ) = inf ( M , RR* , < ) )
Theorem	ovnval2b 38437*	Value of the Lebesgue outer measure of a subset A of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- L = ( a e. ~P ( RR ^m X ) |-> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )   =>    |- ( ph -> ( (voln* ` X ) ` A ) = if ( X = (/) , 0 , inf ( ( L ` A ) , RR* , < ) ) )
Theorem	volicorescl 38438	The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( A e. ran ( [,) |` ( RR X. RR ) ) -> ( vol ` A ) e. RR )
Theorem	ovnprodcl 38439*	The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- ( ph -> F : NN --> ( ( RR X. RR ) ^m X ) )   &    |- ( ph -> I e. NN )   =>    |- ( ph -> prod_ k e. X ( vol ` ( ( [,) o. ( F ` I ) ) ` k ) ) e. ( 0 [,) +oo ) )
Theorem	hoiprodcl2 38440*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )   &    |- ( ph -> I : X --> ( RR X. RR ) )   =>    |- ( ph -> ( L ` I ) e. ( 0 [,) +oo ) )
Theorem	hoicvrrex 38441*	Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ ( RR ^m X ) )   =>    |- ( ph -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ +oo = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
Theorem	ovnsupge0 38442*	The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   =>    |- ( ph -> M C_ ( 0 [,] +oo ) )
Theorem	ovnlecvr 38443*	Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with X the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )   &    |- ( ph -> I : NN --> ( ( RR X. RR ) ^m X ) )   &    |- ( ph -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )   =>    |- ( ph -> ( (voln* ` X ) ` A ) <_ (Σ^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) )
Theorem	ovnpnfelsup 38444*	+oo is an element of the set used in the definition of the Lebesgue outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   =>    |- ( ph -> +oo e. M )
Theorem	ovnsslelem 38445*	The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> B C_ ( RR ^m X ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   &    |- N = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   =>    |- ( ph -> ( (voln* ` X ) ` A ) <_ ( (voln* ` X ) ` B ) )
Theorem	ovnssle 38446	The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ B )   &    |- ( ph -> B C_ ( RR ^m X ) )   =>    |- ( ph -> ( (voln* ` X ) ` A ) <_ ( (voln* ` X ) ` B ) )
Theorem	ovnlerp 38447*	The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- ( ph -> E e. RR+ )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   =>    |- ( ph -> E. z e. M z <_ ( ( (voln* ` X ) ` A ) +e E ) )
Theorem	ovnf 38448	The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> (voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
Theorem	ovncvrrp 38449*	The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- ( ph -> E e. RR+ )   &    |- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )   &    |- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )   &    |- D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | (Σ^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( (voln* ` X ) ` a ) +e e ) } ) )   =>    |- ( ph -> E. i i e. ( ( D ` A ) ` E ) )
Theorem	ovn0lem 38450*	For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) }   &    |- ( ph -> inf ( M , RR* , < ) e. ( 0 [,] +oo ) )   &    |- I = ( j e. NN |-> ( l e. X |-> <. 1 , 0 >. ) )   =>    |- ( ph -> inf ( M , RR* , < ) = 0 )
Theorem	ovn0 38451	For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> ( (voln* ` X ) ` (/) ) = 0 )
Theorem	ovncl 38452	The Lebesgue outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   =>    |- ( ph -> ( (voln* ` X ) ` A ) e. ( 0 [,] +oo ) )
Theorem	ovn02 38453	For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- (voln* ` (/) ) = ( x e. ~P { (/) } |-> 0 )
Theorem	ovnxrcl 38454	The Lebesgue outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   =>    |- ( ph -> ( (voln* ` X ) ` A ) e. RR* )
Theorem	ovnsubaddlem1 38455*	The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : NN --> ~P ( RR ^m X ) )   &    |- ( ph -> E e. RR+ )   &    |- Z = ( a e. ~P ( RR ^m X ) |-> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )   &    |- C = ( a e. ~P ( RR ^m X ) |-> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )   &    |- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )   &    |- D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | (Σ^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( (voln* ` X ) ` a ) +e e ) } ) )   &    |- ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )   &    |- ( ph -> F : NN -1-1-onto-> ( NN X. NN ) )   &    |- G = ( m e. NN |-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )   =>    |- ( ph -> ( (voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( (Σ^ ` ( n e. NN |-> ( (voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
Theorem	ovnsubaddlem2 38456*	(voln* ` X ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : NN --> ~P ( RR ^m X ) )   &    |- ( ph -> E e. RR+ )   &    |- Z = ( a e. ~P ( RR ^m X ) |-> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )   &    |- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )   &    |- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )   &    |- D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | (Σ^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( (voln* ` X ) ` a ) +e e ) } ) )   =>    |- ( ph -> ( (voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( (Σ^ ` ( n e. NN |-> ( (voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
Theorem	ovnsubadd 38457*	(voln* ` X ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : NN --> ~P ( RR ^m X ) )   =>    |- ( ph -> ( (voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ (Σ^ ` ( n e. NN |-> ( (voln* ` X ) ` ( A ` n ) ) ) ) )
Theorem	ovnome 38458	(voln* ` X ) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X. Proposition 115D (a) of [Fremlin1] p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> (voln* ` X ) e. OutMeas )
Theorem	vonmea 38459	(voln ` X ) is a measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X. Comments in Definition 115E of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> (voln ` X ) e. Meas )
Theorem	volicon0 38460	The measure of a nonempty left-closed, right-open interval. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( vol ` ( A [,) B ) ) = ( B - A ) )
Theorem	hsphoif 38461*	H is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- H = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> X e. V )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( ( H ` A ) ` B ) : X --> RR )
Theorem	hoidmvval 38462*	The dimensional volume of a multidimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> X e. Fin )   =>    |- ( ph -> ( A ( L ` X ) B ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
Theorem	hoissrrn2 38463*	A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ( ph /\ k e. X ) -> A e. RR )   &    |- ( ( ph /\ k e. X ) -> B e. RR* )   =>    |- ( ph -> X_ k e. X ( A [,) B ) C_ ( RR ^m X ) )
Theorem	hsphoival 38464*	H is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- H = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> X e. V )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> K e. X )   =>    |- ( ph -> ( ( ( H ` A ) ` B ) ` K ) = if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) )
Theorem	hoiprodcl3 38465*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- ( ( ph /\ k e. X ) -> A e. RR )   &    |- ( ( ph /\ k e. X ) -> B e. RR )   =>    |- ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) e. ( 0 [,) +oo ) )
Theorem	volicore 38466	The Lebesgue measure of a left-closed right-open interval is a real number. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR )
Theorem	hoidmvcl 38467*	The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) B ) e. ( 0 [,) +oo ) )
Theorem	hoidmv0val 38468*	The dimensional volume of a 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> A : (/) --> RR )   &    |- ( ph -> B : (/) --> RR )   =>    |- ( ph -> ( A ( L ` (/) ) B ) = 0 )
Theorem	hoidmvn0val 38469*	The dimensional volume of a non 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
Theorem	hsphoidmvle2 38470*	The dimensional volume of a half-open interval intersected with a two half-spaces. Used in the last inequality of step (c) of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- X = ( Y u. { Z } )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C <_ D )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) ( ( H ` D ) ` B ) ) )
Theorem	hsphoidmvle 38471*	The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- X = ( Y u. { Z } )   &    |- ( ph -> C e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) B ) )
Theorem	hoidmvval0 38472*	The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ j ph   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> E. j e. X ( B ` j ) <_ ( A ` j ) )   =>    |- ( ph -> ( A ( L ` X ) B ) = 0 )
Theorem	hoiprodp1 38473*	The dimensional volume of a half-open interval with dimension n + 1. Used in the first equality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. Y )   &    |- X = ( Y u. { Z } )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- G = prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) = ( G x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )
Theorem	sge0hsphoire 38474*	If the generalized sum of dimensional volumes of n-dimensional half-open intervals is finite, then the sum stays finite if every half-open interval is intersected with a half-space. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. ( W \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- ( ph -> S e. RR )   =>    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
Theorem	hoidmvval0b 38475*	The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) A ) = 0 )
Theorem	hoidmv1lelem1 38476*	The supremum of U belongs to U. This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> C : NN --> RR )   &    |- ( ph -> D : NN --> RR )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )   &    |- U = { z e. ( A [,] B ) | ( z - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   =>    |- ( ph -> ( S e. U /\ A e. U /\ E. x e. RR A. y e. U y <_ x ) )
Theorem	hoidmv1lelem2 38477*	This is the contradiction proven in step (c) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C : NN --> RR )   &    |- ( ph -> D : NN --> RR )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )   &    |- U = { z e. ( A [,] B ) | ( z - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }   &    |- ( ph -> S e. U )   &    |- ( ph -> A <_ S )   &    |- ( ph -> S < B )   &    |- ( ph -> K e. NN )   &    |- ( ph -> S e. ( ( C ` K ) [,) ( D ` K ) ) )   &    |- M = if ( ( D ` K ) <_ B , ( D ` K ) , B )   =>    |- ( ph -> E. u e. U S < u )
Theorem	hoidmv1lelem3 38478*	The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the non-empty, finite generalized sum, sub case in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> C : NN --> RR )   &    |- ( ph -> D : NN --> RR )   &    |- ( ph -> ( A [,) B ) C_ U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )   &    |- U = { z e. ( A [,] B ) | ( z - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   =>    |- ( ph -> ( B - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
Theorem	hoidmv1le 38479*	The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> Z e. V )   &    |- X = { Z }   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> C : NN --> ( RR ^m X ) )   &    |- ( ph -> D : NN --> ( RR ^m X ) )   &    |- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
Theorem	hoidmvlelem1 38480*	The supremum of U belongs to U. Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   &    |- ( ph -> ( A ` Z ) < ( B ` Z ) )   =>    |- ( ph -> S e. U )
Theorem	hoidmvlelem2 38481*	This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- F = ( y e. Y |-> 0 )   &    |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- ( ph -> S e. U )   &    |- ( ph -> S < ( B ` Z ) )   &    |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )   &    |- O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )   &    |- V = ( { ( B ` Z ) } u. O )   &    |- Q = inf ( V , RR , < )   =>    |- ( ph -> E. u e. U S < u )
Theorem	hoidmvlelem3 38482*	This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )   &    |- F = ( y e. Y |-> 0 )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- ( ph -> S e. U )   &    |- ( ph -> S < ( B ` Z ) )   &    |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )   &    |- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )   &    |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   &    |- O = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )   =>    |- ( ph -> E. u e. U S < u )
Theorem	hoidmvlelem4 38483*	The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29, case nonempty interval and dimension of the space greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Y =/= (/) )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   &    |- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )   &    |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   =>    |- ( ph -> ( A ( L ` W ) B ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )
Theorem	hoidmvlelem5 38484*	The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )   &    |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   &    |- ( ph -> Y =/= (/) )   =>    |- ( ph -> ( A ( L ` W ) B ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
Theorem	hoidmvle 38485*	The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> C : NN --> ( RR ^m X ) )   &    |- ( ph -> D : NN --> ( RR ^m X ) )   &    |- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
Theorem	ovnhoilem1 38486*	The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   &    |- H = ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )   =>    |- ( ph -> ( (voln* ` X ) ` I ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
Theorem	ovnhoilem2 38487*	The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   &    |- F = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )   &    |- S = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) <_ ( (voln* ` X ) ` I ) )
Theorem	ovnhoi 38488*	The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   =>    |- ( ph -> ( (voln* ` X ) ` I ) = ( A ( L ` X ) B ) )
Theorem	dmovn 38489	The domain of the Lebesgue outer measure is the power set of the n-dimensional Real numbers. Step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30 (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> dom (voln* ` X ) = ~P ( RR ^m X ) )
Theorem	hoicoto2 38490*	The half-open interval expressed using a composition of a function into ( RR X. RR ) and using two distinct real valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> I : X --> ( RR X. RR ) )   &    |- A = ( k e. X |-> ( 1st ` ( I ` k ) ) )   &    |- B = ( k e. X |-> ( 2nd ` ( I ` k ) ) )   =>    |- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
Theorem	dmvon 38491	Lebesgue measurable n-dimensional subsets of Reals. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> dom (voln ` X ) = (CaraGen ` (voln* ` X ) ) )
Theorem	hoi2toco 38492*	The half-open interval expressed using a composition of a function into ( RR X. RR ) and using two distinct real valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/ k ph   &    |- I = ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. )   =>    |- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
Theorem	hoidifhspval 38493*	D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- D = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) ) ) )   &    |- ( ph -> Y e. RR )   =>    |- ( ph -> ( D ` Y ) = ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) )
Theorem	hspval 38494*	The value of the half-space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- H = ( x e. Fin |-> ( i e. x , y e. RR |-> X_ k e. x if ( k = i , ( -oo (,) y ) , RR ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> I e. X )   &    |- ( ph -> Y e. RR )   =>    |- ( ph -> ( I ( H ` X ) Y ) = X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) )
Theorem	ovnlecvr2 38495*	Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> C : NN --> ( RR ^m X ) )   &    |- ( ph -> D : NN --> ( RR ^m X ) )   &    |- ( ph -> A C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   =>    |- ( ph -> ( (voln* ` X ) ` A ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
Theorem	ovncvr2 38496*	B and T are the left and right side of a cover of A. This cover is made of n-dimensional half open intervals, and approximates the n-dimensional Lebesgue outer volume of A. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A C_ ( RR ^m X ) )   &    |- ( ph -> E e. RR+ )   &    |- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )   &    |- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )   &    |- D = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { i e. ( C ` a ) | (Σ^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( (voln* ` X ) ` a ) +e r ) } ) )   &    |- ( ph -> I e. ( ( D ` A ) ` E ) )   &    |- B = ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) )   &    |- T = ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) )   =>    |- ( ph -> ( ( ( B : NN --> ( RR ^m X ) /\ T : NN --> ( RR ^m X ) ) /\ A C_ U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) /\ (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( (voln* ` X ) ` A ) +e E ) ) )
Theorem	dmovnsal 38497	The domain of the Lebesgue measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   &    |- S = dom (voln ` X )   =>    |- ( ph -> S e. SAlg )
Theorem	unidmovn 38498	Base set of the n-dimensional Lebesgue outer measure (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> U. dom (voln* ` X ) = ( RR ^m X ) )
Theorem	rrnmbl 38499	The set of n-dimensional Real numbers is Lebesgue measurable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> X e. Fin )   =>    |- ( ph -> ( RR ^m X ) e. dom (voln ` X ) )
Theorem	hoidifhspval2 38500*	D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- D = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) ) ) )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> X e. V )   &    |- ( ph -> A : X --> RR )   =>    |- ( ph -> ( ( D ` Y ) ` A ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )