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
less_eq_dom (chi A,X),(R_EAL r) = X
proof
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
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 13; :: thesis: verum
end;
then X c= less_eq_dom (chi A,X),(R_EAL r) by TARSKI:def 3;
hence less_eq_dom (chi A,X),(R_EAL r) = X by XBOOLE_0:def 10; :: thesis: verum
end;
then less_eq_dom (chi A,X),(R_EAL r) in S by PROB_1:11;
hence B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by MEASURE1:19; :: thesis: verum
end;
suppose A4: ( 0 <= r & r < 1 ) ; :: thesis: B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S
A5: less_eq_dom (chi A,X),(R_EAL r) = X \ A
proof
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 A6: 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 A6, MESFUNC1:def 13;
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 A7: 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 A8: x in X \ A ; :: thesis: x in less_eq_dom (chi A,X),(R_EAL r)
then A9: ( x in X & not x in A ) by XBOOLE_0:def 5;
reconsider x = x as Element of X by A8;
A10: (chi A,X) . x = 0. by A9, FUNCT_3:def 3;
x in dom (chi A,X) by A9, FUNCT_3:def 3;
hence x in less_eq_dom (chi A,X),(R_EAL r) by A4, A10, MESFUNC1:def 13; :: thesis: verum
end;
then X \ A c= less_eq_dom (chi A,X),(R_EAL r) by TARSKI:def 3;
hence less_eq_dom (chi A,X),(R_EAL r) = X \ A by A7, XBOOLE_0:def 10; :: thesis: verum
end;
X in S by PROB_1:11;
then less_eq_dom (chi A,X),(R_EAL r) in S by A5, MEASURE1:20;
hence B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by MEASURE1:19; :: thesis: verum
end;
suppose A11: r < 0 ; :: thesis: B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S
less_eq_dom (chi A,X),(R_EAL r) = {}
proof
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
A12: 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 A11, A12, MESFUNC1:def 13; :: thesis: verum
end;
hence less_eq_dom (chi A,X),(R_EAL r) = {} by SUBSET_1:10; :: thesis: verum
end;
hence B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by PROB_1:10; :: 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:32; :: thesis: verum