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_measurable_on B
let S be SigmaField of X; :: thesis: for A, B being Element of S holds chi (A,X) is_measurable_on B
let A, B be Element of S; :: thesis: chi (A,X) is_measurable_on B
for r being real number holds B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S

proof

let r be real number ; :: thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def 1;

now

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_EAL r))) in S

for x being set st x in X holds
x in less_eq_dom ((chi (A,X)),(R_EAL r))

proof

let x be set ; :: thesis: ( x in X implies x in less_eq_dom ((chi (A,X)),(R_EAL r)) )
assume A2: x in X ; :: thesis: x in less_eq_dom ((chi (A,X)),(R_EAL 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

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, MESFUNC1:def 8; :: 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, MESFUNC1:def 8; :: thesis: verum

end;

end;

end;

hence (chi (A,X)) . x <= 1. ; :: thesis: verum

end;

then (chi (A,X)) . x <= R_EAL r by A1, MESFUNC1:def 8, XXREAL_0:2;
hence x in less_eq_dom ((chi (A,X)),(R_EAL r)) by A3, MESFUNC1:def 12; :: thesis: verum

end;

then X c= less_eq_dom ((chi (A,X)),(R_EAL r)) by TARSKI:def 3;
then less_eq_dom ((chi (A,X)),(R_EAL r)) = X by XBOOLE_0:def 10;
then less_eq_dom ((chi (A,X)),(R_EAL r)) in S by PROB_1:5;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL 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_EAL r))) in S

for x being set st x in less_eq_dom ((chi (A,X)),(R_EAL r)) holds
x in X \ A

proof

let x be set ; :: thesis: ( x in less_eq_dom ((chi (A,X)),(R_EAL r)) implies x in X \ A )
assume A5: x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; :: thesis: x in X \ A
then reconsider x = x as Element of X ;
(chi (A,X)) . x <= R_EAL 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_EAL r)) c= X \ A by TARSKI:def 3;
for x being set st x in X \ A holds
x in less_eq_dom ((chi (A,X)),(R_EAL r))

proof

let x be set ; :: thesis: ( x in X \ A implies x in less_eq_dom ((chi (A,X)),(R_EAL r)) )
assume A7: x in X \ A ; :: thesis: x in less_eq_dom ((chi (A,X)),(R_EAL 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_EAL r)) by A4, A10, MESFUNC1:def 12; :: thesis: verum

end;

then X \ A c= less_eq_dom ((chi (A,X)),(R_EAL r)) by TARSKI:def 3;
then A11: less_eq_dom ((chi (A,X)),(R_EAL r)) = X \ A by A6, XBOOLE_0:def 10;
X in S by PROB_1:5;
then less_eq_dom ((chi (A,X)),(R_EAL r)) in S by A11, MEASURE1:6;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by FINSUB_1:def 2; :: thesis: verum

end;

suppose A12: r < 0 ; :: thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S

for x being Element of X holds not x in less_eq_dom ((chi (A,X)),(R_EAL r))

proof

assume ex x being Element of X st x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; :: thesis: contradiction
then consider x being Element of X such that
A13: x in less_eq_dom ((chi (A,X)),(R_EAL r)) ;
0. <= (chi (A,X)) . x

proof

now

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_EAL r)) = {} by SUBSET_1:4;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by PROB_1:4; :: thesis: verum

end;

end;

end;

hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S ; :: thesis: verum

end;

hence chi (A,X) is_measurable_on B by MESFUNC1:28; :: thesis: verum