HomeHome Metamath Proof Explorer
Theorem List (p. 386 of 410)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26627)
  Hilbert Space Explorer  Hilbert Space Explorer
(26628-28150)
  Users' Mathboxes  Users' Mathboxes
(28151-40909)
 

Theorem List for Metamath Proof Explorer - 38501-38600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremovnsubadd 38501*  (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 ) ) ) ) )
 
Theoremovnome 38502  (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 )
 
Theoremvonmea 38503  (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 )
 
Theoremvolicon0 38504 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 ) )
 
Theoremhsphoif 38505*  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 )
 
Theoremhoidmvval 38506* 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
 ) ) ) ) )
 
Theoremhoissrrn2 38507* 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 ) )
 
Theoremhsphoival 38508*  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 ) ) )
 
Theoremhoiprodcl3 38509* 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 ) )
 
Theoremvolicore 38510 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 )
 
Theoremhoidmvcl 38511* 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 ) )
 
Theoremhoidmv0val 38512* 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 )
 
Theoremhoidmvn0val 38513* 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 ) ) ) )
 
Theoremhsphoidmvle2 38514* 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 ) ) )
 
Theoremhsphoidmvle 38515* 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 ) )
 
Theoremhoidmvval0 38516* 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 )
 
Theoremhoiprodp1 38517* 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 ) ) ) ) )
 
Theoremsge0hsphoire 38518* 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 )
 
Theoremhoidmvval0b 38519* 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 )
 
Theoremhoidmv1lelem1 38520* 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 ) )
 
Theoremhoidmv1lelem2 38521* 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 )
 
Theoremhoidmv1lelem3 38522* 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
 ) ) ) ) ) )
 
Theoremhoidmv1le 38523* 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 ) ) ) ) )
 
Theoremhoidmvlelem1 38524* 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 )
 
Theoremhoidmvlelem2 38525* 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 )
 
Theoremhoidmvlelem3 38526* 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 )
 
Theoremhoidmvlelem4 38527* 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 ) ) ) ) ) )
 
Theoremhoidmvlelem5 38528* 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 ) ) ) ) )
 
Theoremhoidmvle 38529* 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 ) ) ) ) )
 
Theoremovnhoilem1 38530* 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 ) ) ) )
 
Theoremovnhoilem2 38531* 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
 ) )
 
Theoremovnhoi 38532* 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 ) )
 
Theoremdmovn 38533 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 ) )
 
Theoremhoicoto2 38534* 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
 ) ) )
 
Theoremdmvon 38535 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 ) ) )
 
Theoremhoi2toco 38536* 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
 ) ) )
 
Theoremhoidifhspval 38537*  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 ) ) ) ) )
 
Theoremhspval 38538* 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 )
 )
 
Theoremovnlecvr2 38539* 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 ) ) ) ) )
 
Theoremovncvr2 38540*  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 ) ) )
 
Theoremdmovnsal 38541 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 )
 
Theoremunidmovn 38542 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 ) )
 
Theoremrrnmbl 38543 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 )
 )
 
Theoremhoidifhspval2 38544*  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 ) ) ) )
 
Theoremhspdifhsp 38545* A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X  =/= 
 (/) )   &    |-  ( ph  ->  A : X --> RR )   &    |-  ( ph  ->  B : X --> RR )   &    |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ i  e.  x  if ( i  =  l ,  ( -oo (,) y ) ,  RR ) ) )   =>    |-  ( ph  ->  X_ i  e.  X  (
 ( A `  i
 ) [,) ( B `  i ) )  = 
 |^|_ i  e.  X  ( ( i ( H `  X ) ( B `  i
 ) )  \  (
 i ( H `  X ) ( A `
  i ) ) ) )
 
Theoremunidmvon 38546 Base set of the n-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  S  =  dom  (voln `  X )   =>    |-  ( ph  ->  U. S  =  ( RR  ^m  X ) )
 
Theoremhoidifhspf 38547*  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 ) : X --> RR )
 
Theoremhoidifhspval3 38548*  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  ->  J  e.  X )   =>    |-  ( ph  ->  ( ( ( D `  Y ) `  A ) `  J )  =  if ( J  =  K ,  if ( Y  <_  ( A `  J ) ,  ( A `  J ) ,  Y ) ,  ( A `  J ) ) )
 
Theoremhoidifhspdmvle 38549* The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-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  ->  K  e.  X )   &    |-  D  =  ( x  e.  RR  |->  ( c  e.  ( RR  ^m  X )  |->  ( h  e.  X  |->  if ( h  =  K ,  if ( x  <_  (
 c `  h ) ,  ( c `  h ) ,  x ) ,  ( c `  h ) ) ) ) )   &    |-  ( ph  ->  Y  e.  RR )   =>    |-  ( ph  ->  ( ( ( D `  Y ) `  A ) ( L `  X ) B ) 
 <_  ( A ( L `
  X ) B ) )
 
Theoremvoncmpl 38550 The Lebesgue measure is complete. See Definition 112Df of [Fremlin1] p. 19. This is an observation written after Definition 115E of [Fremlin1] p. 31 (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  S  =  dom  (voln `  X )   &    |-  ( ph  ->  E  e.  dom  (voln `  X ) )   &    |-  ( ph  ->  ( (voln `  X ) `  E )  =  0 )   &    |-  ( ph  ->  F 
 C_  E )   =>    |-  ( ph  ->  F  e.  S )
 
Theoremhoiqssbllem1 38551* The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  F/ i ph   &    |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X  =/=  (/) )   &    |-  ( ph  ->  Y  e.  ( RR  ^m  X ) )   &    |-  ( ph  ->  C : X
 --> RR )   &    |-  ( ph  ->  D : X --> RR )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ( ph  /\  i  e.  X )  ->  ( C `  i )  e.  ( ( ( Y `
  i )  -  ( E  /  (
 2  x.  ( sqr `  ( # `  X ) ) ) ) ) (,) ( Y `
  i ) ) )   &    |-  ( ( ph  /\  i  e.  X ) 
 ->  ( D `  i
 )  e.  ( ( Y `  i ) (,) ( ( Y `
  i )  +  ( E  /  (
 2  x.  ( sqr `  ( # `  X ) ) ) ) ) ) )   =>    |-  ( ph  ->  Y  e.  X_ i  e.  X  ( ( C `  i ) [,) ( D `  i ) ) )
 
Theoremhoiqssbllem2 38552* The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  F/ i ph   &    |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X  =/=  (/) )   &    |-  ( ph  ->  Y  e.  ( RR  ^m  X ) )   &    |-  ( ph  ->  C : X
 --> RR )   &    |-  ( ph  ->  D : X --> RR )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ( ph  /\  i  e.  X )  ->  ( C `  i )  e.  ( ( ( Y `
  i )  -  ( E  /  (
 2  x.  ( sqr `  ( # `  X ) ) ) ) ) (,) ( Y `
  i ) ) )   &    |-  ( ( ph  /\  i  e.  X ) 
 ->  ( D `  i
 )  e.  ( ( Y `  i ) (,) ( ( Y `
  i )  +  ( E  /  (
 2  x.  ( sqr `  ( # `  X ) ) ) ) ) ) )   =>    |-  ( ph  ->  X_ i  e.  X  (
 ( C `  i
 ) [,) ( D `  i ) )  C_  ( Y ( ball `  ( dist `  (ℝ^ `  X ) ) ) E ) )
 
Theoremhoiqssbllem3 38553* A n-dimensional ball contains a non-empty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X  =/= 
 (/) )   &    |-  ( ph  ->  Y  e.  ( RR  ^m  X ) )   &    |-  ( ph  ->  E  e.  RR+ )   =>    |-  ( ph  ->  E. c  e.  ( QQ  ^m  X ) E. d  e.  ( QQ  ^m  X ) ( Y  e.  X_ i  e.  X  ( ( c `
  i ) [,) ( d `  i
 ) )  /\  X_ i  e.  X  ( ( c `
  i ) [,) ( d `  i
 ) )  C_  ( Y ( ball `  ( dist `  (ℝ^ `  X ) ) ) E ) ) )
 
Theoremhoiqssbl 38554* A n-dimensional ball contains a non-empty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  Y  e.  ( RR  ^m  X ) )   &    |-  ( ph  ->  E  e.  RR+ )   =>    |-  ( ph  ->  E. c  e.  ( QQ  ^m  X ) E. d  e.  ( QQ  ^m  X ) ( Y  e.  X_ i  e.  X  ( ( c `
  i ) [,) ( d `  i
 ) )  /\  X_ i  e.  X  ( ( c `
  i ) [,) ( d `  i
 ) )  C_  ( Y ( ball `  ( dist `  (ℝ^ `  X ) ) ) E ) ) )
 
Theoremhspmbllem1 38555* Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (a) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  K  e.  X )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  A : X --> RR )   &    |-  ( ph  ->  B : X --> RR )   &    |-  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 )
 ) ) ) ) )   &    |-  T  =  ( y  e.  RR  |->  ( c  e.  ( RR 
 ^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K }
 ) ,  ( c `
  h ) ,  if ( ( c `
  h )  <_  y ,  ( c `  h ) ,  y
 ) ) ) ) )   &    |-  S  =  ( x  e.  RR  |->  ( c  e.  ( RR 
 ^m  X )  |->  ( h  e.  X  |->  if ( h  =  K ,  if ( x  <_  ( c `  h ) ,  ( c `  h ) ,  x ) ,  ( c `  h ) ) ) ) )   =>    |-  ( ph  ->  ( A ( L `  X ) B )  =  ( ( A ( L `  X ) ( ( T `
  Y ) `  B ) ) +e ( ( ( S `  Y ) `
  A ) ( L `  X ) B ) ) )
 
Theoremhspmbllem2 38556* Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ k  e.  x  if ( k  =  l ,  ( -oo (,) y
 ) ,  RR )
 ) )   &    |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  K  e.  X )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( 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 ) ) )   &    |-  ( ph  ->  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( (
 ( C `  j
 ) `  k ) [,) ( ( D `  j ) `  k
 ) ) ) ) )  <_  ( (
 (voln* `  X ) `  A )  +  E )
 )   &    |-  ( ph  ->  (
 (voln* `  X ) `  A )  e.  RR )   &    |-  ( ph  ->  ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) )  e.  RR )   &    |-  ( ph  ->  ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) )  e.  RR )   &    |-  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 )
 ) ) ) ) )   &    |-  T  =  ( y  e.  RR  |->  ( c  e.  ( RR 
 ^m  X )  |->  ( h  e.  X  |->  if ( h  e.  ( X  \  { K }
 ) ,  ( c `
  h ) ,  if ( ( c `
  h )  <_  y ,  ( c `  h ) ,  y
 ) ) ) ) )   &    |-  S  =  ( x  e.  RR  |->  ( c  e.  ( RR 
 ^m  X )  |->  ( h  e.  X  |->  if ( h  =  K ,  if ( x  <_  ( c `  h ) ,  ( c `  h ) ,  x ) ,  ( c `  h ) ) ) ) )   =>    |-  ( ph  ->  (
 ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) )  +  ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) ) )  <_  ( (
 (voln* `  X ) `  A )  +  E )
 )
 
Theoremhspmbllem3 38557* Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. This proof handles the non-trivial cases (non-zero dimension and finite outer measure) (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ k  e.  x  if ( k  =  l ,  ( -oo (,) y
 ) ,  RR )
 ) )   &    |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  K  e.  X )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  ( (voln* `  X ) `  A )  e.  RR )   &    |-  ( ph  ->  A  C_  ( RR  ^m  X ) )   &    |-  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 ) } ) )   &    |-  B  =  ( j  e.  NN  |->  ( k  e.  X  |->  ( 1st `  (
 ( i `  j
 ) `  k )
 ) ) )   &    |-  T  =  ( j  e.  NN  |->  ( k  e.  X  |->  ( 2nd `  ( (
 i `  j ) `  k ) ) ) )   =>    |-  ( ph  ->  (
 ( (voln* `  X ) `  ( A  i^i  ( K ( H `  X ) Y ) ) ) +e ( (voln* `  X ) `  ( A  \  ( K ( H `  X ) Y ) ) ) )  <_  ( (voln* `  X ) `  A ) )
 
Theoremhspmbl 38558* Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ k  e.  x  if ( k  =  l ,  ( -oo (,) y
 ) ,  RR )
 ) )   &    |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  K  e.  X )   &    |-  ( ph  ->  Y  e.  RR )   =>    |-  ( ph  ->  ( K ( H `  X ) Y )  e.  dom  (voln `  X ) )
 
Theoremhoimbllem 38559* Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X  =/= 
 (/) )   &    |-  S  =  dom  (voln `  X )   &    |-  ( ph  ->  A : X --> RR )   &    |-  ( ph  ->  B : X --> RR )   &    |-  H  =  ( x  e.  Fin  |->  ( l  e.  x ,  y  e.  RR  |->  X_ i  e.  x  if ( i  =  l ,  ( -oo (,) y
 ) ,  RR )
 ) )   =>    |-  ( ph  ->  X_ i  e.  X  ( ( A `
  i ) [,) ( B `  i
 ) )  e.  S )
 
Theoremhoimbl 38560* Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  S  =  dom  (voln `  X )   &    |-  ( ph  ->  A : X --> RR )   &    |-  ( ph  ->  B : X --> RR )   =>    |-  ( ph  ->  X_ i  e.  X  ( ( A `
  i ) [,) ( B `  i
 ) )  e.  S )
 
Theoremopnvonmbllem1 38561* The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  F/ i ph   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  C : X --> QQ )   &    |-  ( ph  ->  D : X --> QQ )   &    |-  ( ph  ->  X_ i  e.  X  ( ( C `  i ) [,) ( D `  i ) ) 
 C_  B )   &    |-  ( ph  ->  B  C_  G )   &    |-  ( ph  ->  Y  e.  X_ i  e.  X  ( ( C `  i ) [,) ( D `  i ) ) )   &    |-  K  =  { h  e.  ( ( QQ  X.  QQ )  ^m  X )  |  X_ i  e.  X  ( ( [,) 
 o.  h ) `  i )  C_  G }   &    |-  H  =  ( i  e.  X  |->  <.
 ( C `  i
 ) ,  ( D `
  i ) >. )   =>    |-  ( ph  ->  E. h  e.  K  Y  e.  X_ i  e.  X  (
 ( [,)  o.  h ) `  i ) )
 
Theoremopnvonmbllem2 38562* An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  S  =  dom  (voln `  X )   &    |-  ( ph  ->  G  e.  ( TopOpen `  (ℝ^ `  X ) ) )   &    |-  K  =  { h  e.  ( ( QQ  X.  QQ )  ^m  X )  |  X_ i  e.  X  ( ( [,)  o.  h ) `  i
 )  C_  G }   =>    |-  ( ph  ->  G  e.  S )
 
Theoremopnvonmbl 38563 An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  S  =  dom  (voln `  X )   &    |-  ( ph  ->  G  e.  ( TopOpen `  (ℝ^ `  X ) ) )   =>    |-  ( ph  ->  G  e.  S )
 
Theoremopnssborel 38564 Open sets of a generalized real Euclidean space are Borel sets (notice that this theorem is even more general, because  X is not required to be a set). (Contributed by Glauco Siliprandi, 3-Jan-2021.)
 |-  A  =  ( TopOpen `  (ℝ^ `  X ) )   &    |-  B  =  (SalGen `  A )   =>    |-  A  C_  B
 
Theoremborelmbl 38565 All Borel subsets of the n-dimensional Real numbers are Lebesgue measurable. This is Proposition 115G (b) of [Fremlin1] p. 32. See also Definition 111G (d) of [Fremlin1] p. 13. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  S  =  dom  (voln `  X )   &    |-  B  =  (SalGen `  ( TopOpen `  (ℝ^ `  X ) ) )   =>    |-  ( ph  ->  B 
 C_  S )
 
Theoremvolicorege0 38566 The Lebesgue measure of a left-closed right-open interval with real bounds, is a nonnegative real number. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A [,) B ) )  e.  ( 0 [,) +oo ) )
 
Theoremisvonmbl 38567* The predicate " A is measurable w.r.t. the n-dimensional Lebesgue measure". A set is measurable if it splits every other set  x in a "nice" way, that is, if the measure of the pieces  x  i^i 
A and  x  \  A sum up to the measure of  x. Definition 114E of [Fremlin1] p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  X  e.  Fin )   =>    |-  ( ph  ->  ( E  e.  dom  (voln `  X )  <->  ( E  C_  ( RR  ^m  X ) 
 /\  A. a  e.  ~P  ( RR  ^m  X ) ( ( (voln* `  X ) `  (
 a  i^i  E )
 ) +e ( (voln* `  X ) `  (
 a  \  E )
 ) )  =  ( (voln* `  X ) `  a
 ) ) ) )
 
Theoremmblvon 38568 The n-dimensional Lebesgue measure of a measurable set is the same as its n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  A  e.  dom  (voln `  X ) )   =>    |-  ( ph  ->  (
 (voln `  X ) `  A )  =  ( (voln* `  X ) `  A ) )
 
Theoremvonmblss 38569 n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

 |-  ( ph  ->  X  e.  Fin )   =>    |-  ( ph  ->  dom  (voln `  X )  C_  ~P ( RR  ^m  X ) )
 
Theoremvolico2 38570 The measure of left closed, right open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A [,) B ) )  =  if ( A 
 <_  B ,  ( B  -  A ) ,  0 ) )
 
Theoremvonmblss2 38571 n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  Y  e.  dom  (voln `  X ) )   =>    |-  ( ph  ->  Y  C_  ( RR  ^m  X ) )
 
Theoremovolval2lem 38572* The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X. 
 RR ) ) )   =>    |-  ( ph  ->  ran  seq 1
 (  +  ,  (
 ( abs  o.  -  )  o.  F ) )  = 
 ran  ( n  e. 
 NN  |->  sum_ k  e.  (
 1 ... n ) ( vol `  ( ( [,)  o.  F ) `  k ) ) ) )
 
Theoremovolval2 38573* The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. See ovolval 22481 for an alternative expression. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  C_  RR )   &    |-  M  =  { y  e.  RR*  |  E. f  e.  ( (  <_  i^i  ( RR  X.  RR )
 )  ^m  NN )
 ( A  C_  U. ran  ( (,)  o.  f ) 
 /\  y  =  (Σ^ `  (
 ( abs  o.  -  )  o.  f ) ) ) }   =>    |-  ( ph  ->  ( vol* `  A )  = inf ( M ,  RR*
 ,  <  ) )
 
Theoremovnsubadd2lem 38574*  (voln* `  X ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  A  C_  ( RR  ^m  X ) )   &    |-  ( ph  ->  B 
 C_  ( RR  ^m  X ) )   &    |-  C  =  ( n  e.  NN  |->  if ( n  =  1 ,  A ,  if ( n  =  2 ,  B ,  (/) ) ) )   =>    |-  ( ph  ->  (
 (voln* `  X ) `  ( A  u.  B ) ) 
 <_  ( ( (voln* `  X ) `  A ) +e ( (voln* `  X ) `  B ) ) )
 
Theoremovnsubadd2 38575  (voln* `  X ) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  A  C_  ( RR  ^m  X ) )   &    |-  ( ph  ->  B 
 C_  ( RR  ^m  X ) )   =>    |-  ( ph  ->  ( (voln* `  X ) `  ( A  u.  B ) ) 
 <_  ( ( (voln* `  X ) `  A ) +e ( (voln* `  X ) `  B ) ) )
 
Theoremovolval3 38576* The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^ and  vol  o.  (,). See ovolval 22481 and ovolval2 38573 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  C_  RR )   &    |-  M  =  { y  e.  RR*  |  E. f  e.  ( (  <_  i^i  ( RR  X.  RR )
 )  ^m  NN )
 ( A  C_  U. ran  ( (,)  o.  f ) 
 /\  y  =  (Σ^ `  (
 ( vol  o.  (,) )  o.  f ) ) ) }   =>    |-  ( ph  ->  ( vol* `  A )  = inf ( M ,  RR*
 ,  <  ) )
 
Theoremovnsplit 38577 The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  A  C_  ( RR  ^m  X ) )   =>    |-  ( ph  ->  (
 (voln* `  X ) `  A )  <_  ( ( (voln* `  X ) `  ( A  i^i  B ) ) +e
 ( (voln* `  X ) `  ( A  \  B ) ) ) )
 
Theoremovolval4lem1 38578* |- ( ( ph /\ n e. A ) -> ( ( (,) o. G )  n )  =  ( ( (,)  o.  F
) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  F : NN --> ( RR*  X.  RR* )
 )   &    |-  G  =  ( n  e.  NN  |->  <. ( 1st `  ( F `  n ) ) ,  if ( ( 1st `  ( F `  n ) ) 
 <_  ( 2nd `  ( F `  n ) ) ,  ( 2nd `  ( F `  n ) ) ,  ( 1st `  ( F `  n ) ) ) >. )   &    |-  A  =  { n  e.  NN  |  ( 1st `  ( F `  n ) )  <_  ( 2nd `  ( F `  n ) ) }   =>    |-  ( ph  ->  ( U. ran  ( (,)  o.  F )  =  U. ran  ( (,)  o.  G )  /\  ( vol  o.  ( (,) 
 o.  F ) )  =  ( vol  o.  ( (,)  o.  G ) ) ) )
 
Theoremovolval4lem2 38579* The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 38576, but here  f is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  C_  RR )   &    |-  M  =  { y  e.  RR*  |  E. f  e.  ( ( RR  X.  RR )  ^m  NN )
 ( A  C_  U. ran  ( (,)  o.  f ) 
 /\  y  =  (Σ^ `  (
 ( vol  o.  (,) )  o.  f ) ) ) }   &    |-  G  =  ( n  e.  NN  |->  <.
 ( 1st `  ( f `  n ) ) ,  if ( ( 1st `  ( f `  n ) )  <_  ( 2nd `  ( f `  n ) ) ,  ( 2nd `  ( f `  n ) ) ,  ( 1st `  (
 f `  n )
 ) ) >. )   =>    |-  ( ph  ->  ( vol* `  A )  = inf ( M ,  RR* ,  <  )
 )
 
Theoremovolval4 38580* The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 38576, but here  f may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  C_  RR )   &    |-  M  =  { y  e.  RR*  |  E. f  e.  ( ( RR  X.  RR )  ^m  NN )
 ( A  C_  U. ran  ( (,)  o.  f ) 
 /\  y  =  (Σ^ `  (
 ( vol  o.  (,) )  o.  f ) ) ) }   =>    |-  ( ph  ->  ( vol* `  A )  = inf ( M ,  RR*
 ,  <  ) )
 
Theoremovolval5lem1 38581* |- ( ph -> ( sum^  ( n  e.  NN  |->  ( vol ( ( A - ( W / ( 2 ^ n ) ) ) (,) B ) ) ) ) <_ ( ( sum^ 
( n  e.  NN  |->  ( vol ( A [,) B ) ) ) ) +e W ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  (
 ( ph  /\  n  e. 
 NN )  ->  A  e.  RR )   &    |-  ( ( ph  /\  n  e.  NN )  ->  B  e.  RR )   &    |-  ( ph  ->  W  e.  RR+ )   &    |-  C  =  { n  e.  NN  |  A  <  B }   =>    |-  ( ph  ->  (Σ^ `  ( n  e.  NN  |->  ( vol `  ( ( A  -  ( W  /  (
 2 ^ n ) ) ) (,) B ) ) ) ) 
 <_  ( (Σ^ `  ( n  e.  NN  |->  ( vol `  ( A [,) B ) ) ) ) +e W ) )
 
Theoremovolval5lem2 38582* |- ( ( ph /\ n e. NN ) -> <. ( ( 1st  ( F n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd  ( F n ) ) >. e. ( RR X. RR ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  Q  =  { z  e.  RR*  | 
 E. f  e.  (
 ( RR  X.  RR )  ^m  NN ) ( A  C_  U. ran  ( (,)  o.  f )  /\  z  =  (Σ^ `  ( ( vol  o.  (,) )  o.  f
 ) ) ) }   &    |-  ( ph  ->  Y  =  (Σ^ `  (
 ( vol  o.  [,) )  o.  F ) ) )   &    |-  Z  =  (Σ^ `  ( ( vol  o.  (,) )  o.  G ) )   &    |-  ( ph  ->  F : NN --> ( RR 
 X.  RR ) )   &    |-  ( ph  ->  A  C_  U. ran  ( [,)  o.  F ) )   &    |-  ( ph  ->  W  e.  RR+ )   &    |-  G  =  ( n  e.  NN  |->  <.
 ( ( 1st `  ( F `  n ) )  -  ( W  /  ( 2 ^ n ) ) ) ,  ( 2nd `  ( F `  n ) )
 >. )   =>    |-  ( ph  ->  E. z  e.  Q  z  <_  ( Y +e W ) )
 
Theoremovolval5lem3 38583* The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  M  =  { y  e.  RR*  | 
 E. f  e.  (
 ( RR  X.  RR )  ^m  NN ) ( A  C_  U. ran  ( [,)  o.  f )  /\  y  =  (Σ^ `  ( ( vol  o.  [,) )  o.  f
 ) ) ) }   &    |-  Q  =  { z  e.  RR*  | 
 E. f  e.  (
 ( RR  X.  RR )  ^m  NN ) ( A  C_  U. ran  ( (,)  o.  f )  /\  z  =  (Σ^ `  ( ( vol  o.  (,) )  o.  f
 ) ) ) }   =>    |- inf ( Q ,  RR* ,  <  )  = inf ( M ,  RR*
 ,  <  )
 
Theoremovolval5 38584* The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  C_  RR )   &    |-  M  =  { y  e.  RR*  |  E. f  e.  ( ( RR  X.  RR )  ^m  NN )
 ( A  C_  U. ran  ( [,)  o.  f ) 
 /\  y  =  (Σ^ `  (
 ( vol  o.  [,) )  o.  f ) ) ) }   =>    |-  ( ph  ->  ( vol* `  A )  = inf ( M ,  RR*
 ,  <  ) )
 
Theoremovnovollem1 38585* if  F is a cover of  B in  RR, then  I is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  F  e.  ( ( RR  X.  RR )  ^m  NN )
 )   &    |-  I  =  ( j  e.  NN  |->  { <. A ,  ( F `  j ) >. } )   &    |-  ( ph  ->  B  C_  U. ran  ( [,)  o.  F ) )   &    |-  ( ph  ->  B  e.  W )   &    |-  ( ph  ->  Z  =  (Σ^ `  (
 ( vol  o.  [,) )  o.  F ) ) )   =>    |-  ( ph  ->  E. i  e.  ( ( ( RR 
 X.  RR )  ^m  { A } )  ^m  NN ) ( ( B 
 ^m  { A } )  C_  U_ j  e.  NN  X_ k  e.  { A }  ( ( [,)  o.  ( i `  j
 ) ) `  k
 )  /\  Z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  { A }  ( vol `  (
 ( [,)  o.  (
 i `  j )
 ) `  k )
 ) ) ) ) )
 
Theoremovnovollem2 38586* if  I is a cover of  ( B  ^m  { A }
) in ℝ^ 1, then  F is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  e.  W )   &    |-  ( ph  ->  I  e.  ( ( ( RR  X.  RR )  ^m  { A } )  ^m  NN ) )   &    |-  ( ph  ->  ( B  ^m  { A } )  C_  U_ j  e.  NN  X_ k  e.  { A }  (
 ( [,)  o.  ( I `  j ) ) `
  k ) )   &    |-  ( ph  ->  Z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  { A }  ( vol `  (
 ( [,)  o.  ( I `  j ) ) `
  k ) ) ) ) )   &    |-  F  =  ( j  e.  NN  |->  ( ( I `  j ) `  A ) )   =>    |-  ( ph  ->  E. f  e.  ( ( RR  X.  RR )  ^m  NN )
 ( B  C_  U. ran  ( [,)  o.  f ) 
 /\  Z  =  (Σ^ `  (
 ( vol  o.  [,) )  o.  f ) ) ) )
 
Theoremovnovollem3 38587* The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  C_ 
 RR )   &    |-  M  =  {
 z  e.  RR*  |  E. i  e.  ( (
 ( RR  X.  RR )  ^m  { A }
 )  ^m  NN )
 ( ( B  ^m  { A } )  C_  U_ j  e.  NN  X_ k  e.  { A }  (
 ( [,)  o.  (
 i `  j )
 ) `  k )  /\  z  =  (Σ^ `  (
 j  e.  NN  |->  prod_
 k  e.  { A }  ( vol `  (
 ( [,)  o.  (
 i `  j )
 ) `  k )
 ) ) ) ) }   &    |-  N  =  {
 z  e.  RR*  |  E. f  e.  ( ( RR  X.  RR )  ^m  NN ) ( B  C_  U.
 ran  ( [,)  o.  f )  /\  z  =  (Σ^ `  ( ( vol  o.  [,) )  o.  f
 ) ) ) }   =>    |-  ( ph  ->  ( (voln* ` 
 { A } ) `  ( B  ^m  { A } ) )  =  ( vol* `  B ) )
 
Theoremovnovol 38588 The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  C_ 
 RR )   =>    |-  ( ph  ->  (
 (voln* ` 
 { A } ) `  ( B  ^m  { A } ) )  =  ( vol* `  B ) )
 
Theoremvonvolmbllem 38589* If a subset  B of real numbers is Lebesgue measurable, then its corresponding 1-dimensional set is measurable w.r.t. the n-dimensional Lebesgue measure, (with  n equal to  1). (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  C_ 
 RR )   &    |-  ( ph  ->  A. y  e.  ~P  RR ( vol* `  y
 )  =  ( ( vol* `  (
 y  i^i  B )
 ) +e ( vol* `  (
 y  \  B )
 ) ) )   &    |-  ( ph  ->  X  C_  ( RR  ^m  { A }
 ) )   &    |-  Y  =  U_ f  e.  X  ran  f   =>    |-  ( ph  ->  (
 ( (voln* ` 
 { A } ) `  ( X  i^i  ( B  ^m  { A }
 ) ) ) +e ( (voln* ` 
 { A } ) `  ( X  \  ( B  ^m  { A }
 ) ) ) )  =  ( (voln* ` 
 { A } ) `  X ) )
 
Theoremvonvolmbl 38590 A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  C_ 
 RR )   =>    |-  ( ph  ->  (
 ( B  ^m  { A } )  e.  dom  (voln `  { A }
 ) 
 <->  B  e.  dom  vol ) )
 
Theoremvonvol 38591 The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  e.  dom  vol )   =>    |-  ( ph  ->  (
 (voln `  { A }
 ) `  ( B  ^m  { A } )
 )  =  ( vol `  B ) )
 
Theoremvonvolmbl2 38592* A subset  X of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection  Y on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  F/_ f Y   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  X 
 C_  ( RR  ^m  { A } ) )   &    |-  Y  =  U_ f  e.  X  ran  f   =>    |-  ( ph  ->  ( X  e.  dom  (voln ` 
 { A } )  <->  Y  e.  dom  vol ) )
 
Theoremvonvol2 38593* The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
 |-  F/_ f Y   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  X  e.  dom  (voln `  { A } ) )   &    |-  Y  =  U_ f  e.  X  ran  f   =>    |-  ( ph  ->  (
 (voln `  { A }
 ) `  X )  =  ( vol `  Y ) )
 
21.31  Mathbox for Saveliy Skresanov
 
21.31.1  Ceva's theorem
 
Theoremsigarval 38594* Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A G B )  =  ( Im `  ( ( * `
  A )  x.  B ) ) )
 
Theoremsigarim 38595* Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A G B )  e.  RR )
 
Theoremsigarac 38596* Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A G B )  =  -u ( B G A ) )
 
Theoremsigaraf 38597* Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( ( A  +  C ) G B )  =  ( ( A G B )  +  ( C G B ) ) )
 
Theoremsigarmf 38598* Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( ( A  -  C ) G B )  =  ( ( A G B )  -  ( C G B ) ) )
 
Theoremsigaras 38599* Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A G ( B  +  C ) )  =  ( ( A G B )  +  ( A G C ) ) )
 
Theoremsigarms 38600* Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A G ( B  -  C ) )  =  ( ( A G B )  -  ( A G C ) ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31500 316 31501-31600 317 31601-31700 318 31701-31800 319 31801-31900 320 31901-32000 321 32001-32100 322 32101-32200 323 32201-32300 324 32301-32400 325 32401-32500 326 32501-32600 327 32601-32700 328 32701-32800 329 32801-32900 330 32901-33000 331 33001-33100 332 33101-33200 333 33201-33300 334 33301-33400 335 33401-33500 336 33501-33600 337 33601-33700 338 33701-33800 339 33801-33900 340 33901-34000 341 34001-34100 342 34101-34200 343 34201-34300 344 34301-34400 345 34401-34500 346 34501-34600 347 34601-34700 348 34701-34800 349 34801-34900 350 34901-35000 351 35001-35100 352 35101-35200 353 35201-35300 354 35301-35400 355 35401-35500 356 35501-35600 357 35601-35700 358 35701-35800 359 35801-35900 360 35901-36000 361 36001-36100 362 36101-36200 363 36201-36300 364 36301-36400 365 36401-36500 366 36501-36600 367 36601-36700 368 36701-36800 369 36801-36900 370 36901-37000 371 37001-37100 372 37101-37200 373 37201-37300 374 37301-37400 375 37401-37500 376 37501-37600 377 37601-37700 378 37701-37800 379 37801-37900 380 37901-38000 381 38001-38100 382 38101-38200 383 38201-38300 384 38301-38400 385 38401-38500 386 38501-38600 387 38601-38700 388 38701-38800 389 38801-38900 390 38901-39000 391 39001-39100 392 39101-39200 393 39201-39300 394 39301-39400 395 39401-39500 396 39501-39600 397 39601-39700 398 39701-39800 399 39801-39900 400 39901-40000 401 40001-40100 402 40101-40200 403 40201-40300 404 40301-40400 405 40401-40500 406 40501-40600 407 40601-40700 408 40701-40800 409 40801-40900 410 40901-40909
  Copyright terms: Public domain < Previous  Next >