let X be non empty set ; :: thesis: for S being SigmaField of X
for A, B being Element of S holds chi (A,X) is B -measurable
let S be SigmaField of X; :: thesis: for A, B being Element of S holds chi (A,X) is B -measurable
let A, B be Element of S; :: thesis: chi (A,X) is B -measurable
for r being Real holds B /\ (less_eq_dom ((chi (A,X)),r)) in S
proof
let r be Real; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S
reconsider r = r as Real ;
now :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S
per cases ( r >= 1 or ( 0 <= r & r < 1 ) or r < 0 ) ;
suppose A1: r >= 1 ; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S
for x being object st x in X holds
x in less_eq_dom ((chi (A,X)),r)
proof
let x be object ; :: thesis: ( x in X implies x in less_eq_dom ((chi (A,X)),r) )
assume A2: x in X ; :: thesis: x in less_eq_dom ((chi (A,X)),r)
then A3: x in dom (chi (A,X)) by FUNCT_3:def 3;
reconsider x = x as Element of X by A2;
(chi (A,X)) . x <= 1.
proof
now :: thesis: (chi (A,X)) . x <= 1.
per cases ( x in A or not x in A ) ;
suppose x in A ; :: thesis: (chi (A,X)) . x <= 1.
hence (chi (A,X)) . x <= 1. by FUNCT_3:def 3; :: thesis: verum
end;
suppose not x in A ; :: thesis: (chi (A,X)) . x <= 1.
hence (chi (A,X)) . x <= 1. by FUNCT_3:def 3; :: thesis: verum
end;
end;
end;
hence (chi (A,X)) . x <= 1. ; :: thesis: verum
end;
then (chi (A,X)) . x <= r by A1, XXREAL_0:2;
hence x in less_eq_dom ((chi (A,X)),r) by A3, MESFUNC1:def 12; :: thesis: verum
end;
then X c= less_eq_dom ((chi (A,X)),r) ;
then less_eq_dom ((chi (A,X)),r) = X ;
then less_eq_dom ((chi (A,X)),r) in S by PROB_1:5;
hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by FINSUB_1:def 2; :: thesis: verum
end;
suppose A4: ( 0 <= r & r < 1 ) ; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S
for x being object st x in less_eq_dom ((chi (A,X)),r) holds
x in X \ A
proof
let x be object ; :: thesis: ( x in less_eq_dom ((chi (A,X)),r) implies x in X \ A )
assume A5: x in less_eq_dom ((chi (A,X)),r) ; :: thesis: x in X \ A
then reconsider x = x as Element of X ;
(chi (A,X)) . x <= r by A5, MESFUNC1:def 12;
then not x in A by A4, FUNCT_3:def 3;
hence x in X \ A by XBOOLE_0:def 5; :: thesis: verum
end;
then A6: less_eq_dom ((chi (A,X)),r) c= X \ A ;
for x being object st x in X \ A holds
x in less_eq_dom ((chi (A,X)),r)
proof
let x be object ; :: thesis: ( x in X \ A implies x in less_eq_dom ((chi (A,X)),r) )
assume A7: x in X \ A ; :: thesis: x in less_eq_dom ((chi (A,X)),r)
then A8: x in X ;
A9: not x in A by A7, XBOOLE_0:def 5;
reconsider x = x as Element of X by A7;
A10: (chi (A,X)) . x = 0. by A9, FUNCT_3:def 3;
x in dom (chi (A,X)) by A8, FUNCT_3:def 3;
hence x in less_eq_dom ((chi (A,X)),r) by A4, A10, MESFUNC1:def 12; :: thesis: verum
end;
then X \ A c= less_eq_dom ((chi (A,X)),r) ;
then A11: less_eq_dom ((chi (A,X)),r) = X \ A by A6;
X in S by PROB_1:5;
then less_eq_dom ((chi (A,X)),r) in S by A11, MEASURE1:6;
hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by FINSUB_1:def 2; :: thesis: verum
end;
suppose A12: r < 0 ; :: thesis: B /\ (less_eq_dom ((chi (A,X)),r)) in S
for x being Element of X holds not x in less_eq_dom ((chi (A,X)),r)
proof
assume ex x being Element of X st x in less_eq_dom ((chi (A,X)),r) ; :: thesis: contradiction
then consider x being Element of X such that
A13: x in less_eq_dom ((chi (A,X)),r) ;
0. <= (chi (A,X)) . x
proof
now :: thesis: 0. <= (chi (A,X)) . x
per cases ( x in A or not x in A ) ;
suppose x in A ; :: thesis: 0. <= (chi (A,X)) . x
hence 0. <= (chi (A,X)) . x by FUNCT_3:def 3; :: thesis: verum
end;
suppose not x in A ; :: thesis: 0. <= (chi (A,X)) . x
hence 0. <= (chi (A,X)) . x by FUNCT_3:def 3; :: thesis: verum
end;
end;
end;
hence 0. <= (chi (A,X)) . x ; :: thesis: verum
end;
hence contradiction by A12, A13, MESFUNC1:def 12; :: thesis: verum
end;
then less_eq_dom ((chi (A,X)),r) = {} by SUBSET_1:4;
hence B /\ (less_eq_dom ((chi (A,X)),r)) in S by PROB_1:4; :: thesis: verum
end;
end;
end;
hence B /\ (less_eq_dom ((chi (A,X)),r)) in S ; :: thesis: verum
end;
hence chi (A,X) is B -measurable by MESFUNC1:28; :: thesis: verum