let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds
( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )
let Sigma be SigmaField of Omega; :: thesis: for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds
( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )
let X be Function of Omega,REAL; :: thesis: ( X is Sigma, Borel_Sets -random_variable-like implies ( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) ) )
assume A1: X is Sigma, Borel_Sets -random_variable-like ; :: thesis: ( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )
A2: for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma )
proof
let k be Real; :: thesis: ( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma )
A3: for q being set holds
( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) )
proof
let q be set ; :: thesis: ( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) )
now :: thesis: ( ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) implies ex w being Element of Omega st
( q = w & X . w >= k ) )
assume ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ; :: thesis: ex w being Element of Omega st
( q = w & X . w >= k )
then consider w being Element of Omega such that
A4: ( q = w & X . w in [.k,+infty.] ) ;
X . w in { z where z is Element of ExtREAL : ( k <= z & z <= +infty ) } by A4, XXREAL_1:def 1;
then ex z being Element of ExtREAL st
( X . w = z & k <= z & z <= +infty ) ;
hence ex w being Element of Omega st
( q = w & X . w >= k ) by A4; :: thesis: verum
end;
hence ( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ) by XXREAL_1:219; :: thesis: verum
end;
A5: for x being object holds
( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w >= k ) ) ;
then A6: ( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w in [.k,+infty.] ) ) by A3;
( x in { w where w is Element of Omega : X . w in [.k,+infty.] } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
proof
hereby :: thesis: ( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } implies x in { w where w is Element of Omega : X . w in [.k,+infty.] } )
assume x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; :: thesis: x in { g where g is Element of Omega : X . g in [.k,+infty.[ }
then consider w being Element of Omega such that
A7: ( w = x & X . w in [.k,+infty.] ) ;
X . w in { a where a is Element of ExtREAL : ( k <= a & a <= +infty ) } by A7, XXREAL_1:def 1;
then consider a being Element of ExtREAL such that
A8: ( X . w = a & k <= a & a <= +infty ) ;
A9: ( X . w = a & k <= a & a < +infty ) by A8, XXREAL_0:9;
{ z where z is Element of ExtREAL : ( k <= z & z < +infty ) } = [.k,+infty.[ by XXREAL_1:def 2;
then X . w in [.k,+infty.[ by A9;
hence x in { g where g is Element of Omega : X . g in [.k,+infty.[ } by A7; :: thesis: verum
end;
assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; :: thesis: x in { w where w is Element of Omega : X . w in [.k,+infty.] }
then consider w being Element of Omega such that
A10: ( w = x & X . w in [.k,+infty.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u < +infty ) } ) by A10, XXREAL_1:def 2;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & k <= u & u < +infty ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u <= +infty ) } ) ;
then ( w = x & X . w in [.k,+infty.] ) by XXREAL_1:def 1;
hence x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; :: thesis: verum
end;
hence ( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ) by A6; :: thesis: verum
end;
k in REAL by XREAL_0:def 1;
then A11: not [.k,+infty.[ is empty by XXREAL_0:9, XXREAL_1:31;
A12: { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
proof
{ w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
proof
for x being object holds
( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } iff x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } iff x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } )
hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } implies x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; :: thesis: x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
then ex w being Element of Omega st
( w = x & X . w in [.k,+infty.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; :: thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; :: thesis: x in { w where w is Element of Omega : X . w in [.k,+infty.[ }
then consider w being Element of Omega such that
A13: ( w = x & X . w is Element of [.k,+infty.[ ) ;
thus x in { w where w is Element of Omega : X . w in [.k,+infty.[ } by A13, A11; :: thesis: verum
end;
hence { w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by TARSKI:2; :: thesis: verum
end;
hence { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by A5, TARSKI:2; :: thesis: verum
end;
A14: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th3;
A15: { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } = X " [.k,+infty.[ by Lm1, A11;
A16: for q being set holds
( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) )
proof
let q be set ; :: thesis: ( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) )
now :: thesis: ( ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) implies ex w being Element of Omega st
( q = w & X . w < k ) )
assume ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ; :: thesis: ex w being Element of Omega st
( q = w & X . w < k )
then consider w being Element of Omega such that
A17: ( q = w & X . w in [.-infty,k.[ ) ;
X . w in { z where z is Element of ExtREAL : ( -infty <= z & z < k ) } by A17, XXREAL_1:def 2;
then ex z being Element of ExtREAL st
( X . w = z & -infty <= z & z < k ) ;
hence ex w being Element of Omega st
( q = w & X . w < k ) by A17; :: thesis: verum
end;
hence ( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ) by XXREAL_1:221; :: thesis: verum
end;
for x being object holds
( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w < k ) ) ;
then A18: ( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w in [.-infty,k.[ ) ) by A16;
( x in { w where w is Element of Omega : X . w in [.-infty,k.[ } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
proof
hereby :: thesis: ( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } implies x in { w where w is Element of Omega : X . w in [.-infty,k.[ } )
assume x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; :: thesis: x in { g where g is Element of Omega : X . g in ].-infty,k.[ }
then consider w being Element of Omega such that
A19: ( w = x & X . w in [.-infty,k.[ ) ;
X . w in { a where a is Element of ExtREAL : ( -infty <= a & a < k ) } by A19, XXREAL_1:def 2;
then consider a being Element of ExtREAL such that
A20: ( X . w = a & -infty <= a & a < k ) ;
A21: ( X . w = a & -infty < a & a < k ) by A20, XXREAL_0:12;
{ z where z is Element of ExtREAL : ( -infty < z & z < k ) } = ].-infty,k.[ by XXREAL_1:def 4;
then X . w in ].-infty,k.[ by A21;
hence x in { g where g is Element of Omega : X . g in ].-infty,k.[ } by A19; :: thesis: verum
end;
assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; :: thesis: x in { w where w is Element of Omega : X . w in [.-infty,k.[ }
then consider w being Element of Omega such that
A22: ( w = x & X . w in ].-infty,k.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( -infty < u & u < k ) } ) by A22, XXREAL_1:def 4;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & -infty < u & u < k ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( -infty <= u & u < k ) } ) ;
then ( w = x & X . w in [.-infty,k.[ ) by XXREAL_1:def 2;
hence x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; :: thesis: verum
end;
hence ( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ) by A18; :: thesis: verum
end;
then A23: { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w in ].-infty,k.[ } by TARSKI:2;
{ w where w is Element of Omega : X . w < k } is Element of Sigma
proof
A24: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th3;
k in REAL by XREAL_0:def 1;
then A25: not ].-infty,k.[ is empty by XXREAL_0:12, XXREAL_1:33;
then A26: { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } = X " ].-infty,k.[ by Lm1;
for x being object holds
( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } iff x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } iff x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } )
hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } implies x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; :: thesis: x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ }
then ex w being Element of Omega st
( w = x & X . w in ].-infty,k.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; :: thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; :: thesis: x in { w where w is Element of Omega : X . w in ].-infty,k.[ }
then consider w being Element of Omega such that
A27: ( w = x & X . w is Element of ].-infty,k.[ ) ;
thus x in { w where w is Element of Omega : X . w in ].-infty,k.[ } by A27, A25; :: thesis: verum
end;
then { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } by A23, TARSKI:2
.= X " ].-infty,k.[ by A26 ;
hence { w where w is Element of Omega : X . w < k } is Element of Sigma by A24, A1; :: thesis: verum
end;
hence ( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) by A14, A1, A12, A15; :: thesis: verum
end;
A28: for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
proof
let k1, k2 be Real; :: thesis: ( k1 < k2 implies { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma )
assume A29: k1 < k2 ; :: thesis: { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
then A30: not [.k1,k2.[ is empty by XXREAL_1:31;
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
proof
for x being object holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } )
hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } implies x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } )
assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } ; :: thesis: x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ }
then consider w being Element of Omega such that
A31: ( x = w & k1 <= X . w & X . w < k2 ) ;
reconsider a = X . w as Element of ExtREAL by XXREAL_0:def 1;
a = X . w ;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z < k2 ) } by A31;
then X . w is Element of [.k1,k2.[ by XXREAL_1:def 2;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ } by A31; :: thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } ; :: thesis: x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) }
then consider w being Element of Omega such that
A32: ( x = w & X . w is Element of [.k1,k2.[ ) ;
A33: not [.k1,k2.[ is empty by A29, XXREAL_1:31;
X . w in [.k1,k2.[ by A32, A33;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a < k2 ) } by XXREAL_1:def 2;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a < k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } by A32; :: thesis: verum
end;
then A34: { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } by TARSKI:2;
A35: ( [.k2,k1.[ is Element of Borel_Sets & [.k1,k2.[ is Element of Borel_Sets ) by Th4;
{ w where w is Element of Omega : X . w is Element of [.k1,k2.[ } = X " [.k1,k2.[ by Lm1, A30;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma by A1, A34, A35; :: thesis: verum
end;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ; :: thesis: verum
end;
A36: for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma
proof
let k1, k2 be Real; :: thesis: ( k1 <= k2 implies { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma )
assume A37: k1 <= k2 ; :: thesis: { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma
then A38: not [.k1,k2.] is empty by XXREAL_1:30;
for x being object holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } )
hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } implies x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } )
assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } ; :: thesis: x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] }
then consider w being Element of Omega such that
A39: ( x = w & k1 <= X . w & X . w <= k2 ) ;
reconsider a = X . w as Element of ExtREAL by XXREAL_0:def 1;
a = X . w ;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z <= k2 ) } by A39;
then X . w is Element of [.k1,k2.] by XXREAL_1:def 1;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] } by A39; :: thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } ; :: thesis: x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) }
then consider w being Element of Omega such that
A40: ( x = w & X . w is Element of [.k1,k2.] ) ;
A41: not [.k1,k2.] is empty by A37, XXREAL_1:30;
X . w in [.k1,k2.] by A40, A41;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a <= k2 ) } by XXREAL_1:def 1;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a <= k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } by A40; :: thesis: verum
end;
then A42: { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.] } by TARSKI:2;
A43: ( [.k1,k2.[ is Element of Borel_Sets & [.k1,k2.] is Element of Borel_Sets ) by Th8, Th4;
{ w where w is Element of Omega : X . w is Element of [.k1,k2.] } = X " [.k1,k2.] by Lm1, A38;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma by A1, A42, A43; :: thesis: verum
end;
A44: for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r }
proof
let r be Real; :: thesis: less_dom (X,r) = { w where w is Element of Omega : X . w < r }
for x being object holds
( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )
proof
let x be object ; :: thesis: ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )
reconsider xx = x as set by TARSKI:1;
( x in less_dom (X,r) iff ( x in dom X & X . xx < r ) ) by MESFUNC1:def 11;
then ( x in less_dom (X,r) iff ( x in Omega & X . xx < r ) ) by FUNCT_2:def 1;
then ( x in less_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q < r ) ) ;
hence ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } ) ; :: thesis: verum
end;
hence less_dom (X,r) = { w where w is Element of Omega : X . w < r } by TARSKI:2; :: thesis: verum
end;
A45: for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }
proof
let r be Real; :: thesis: great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }
for x being object holds
( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )
proof
let x be object ; :: thesis: ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )
reconsider xx = x as set by TARSKI:1;
( x in great_eq_dom (X,r) iff ( x in dom X & X . xx >= r ) ) by MESFUNC1:def 14;
then ( x in great_eq_dom (X,r) iff ( x in Omega & X . xx >= r ) ) by FUNCT_2:def 1;
then ( x in great_eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q >= r ) ) ;
hence ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } ) ; :: thesis: verum
end;
hence great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } by TARSKI:2; :: thesis: verum
end;
A46: for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r }
proof
let r be Real; :: thesis: eq_dom (X,r) = { w where w is Element of Omega : X . w = r }
for x being object holds
( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )
proof
let x be object ; :: thesis: ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )
( x in eq_dom (X,r) iff ( x in dom X & X . x = r ) ) by MESFUNC1:def 15;
then ( x in eq_dom (X,r) iff ( x in Omega & X . x = r ) ) by FUNCT_2:def 1;
then ( x in eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q = r ) ) ;
hence ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } ) ; :: thesis: verum
end;
hence eq_dom (X,r) = { w where w is Element of Omega : X . w = r } by TARSKI:2; :: thesis: verum
end;
for r being Real holds eq_dom (X,r) is Element of Sigma
proof
let r be Real; :: thesis: eq_dom (X,r) is Element of Sigma
for x being object holds
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } )
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } )
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & r <= X . q & X . q <= r ) ) ;
then ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & X . q = r ) ) by XXREAL_0:1;
hence ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } ) ; :: thesis: verum
end;
then { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } = { w where w is Element of Omega : X . w = r } by TARSKI:2;
then { w where w is Element of Omega : X . w = r } is Element of Sigma by A36;
hence eq_dom (X,r) is Element of Sigma by A46; :: thesis: verum
end;
hence ( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) ) by A2, A28, A36, A44, A45, A46; :: thesis: verum