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
A1: 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;
A2: now
per cases ( r >= 1 or ( 0 <= r & r < 1 ) or r < 0 ) ;
suppose A3: r >= 1 ; :: thesis: B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S
A4: 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 A5: x in X ; :: thesis: x in less_eq_dom (chi A,X),(R_EAL r)
A6: x in dom (chi A,X) by A5, FUNCT_3:def 3;
reconsider x = x as Element of X by A5;
A7: (chi A,X) . x <= 1.
proof
thus (chi A,X) . x <= 1. by A8; :: thesis: verum
end;
A11: (chi A,X) . x <= R_EAL r by A3, A7, MESFUNC1:def 8, XXREAL_0:2;
thus x in less_eq_dom (chi A,X),(R_EAL r) by A6, A11, MESFUNC1:def 13; :: thesis: verum
end;
A12: X c= less_eq_dom (chi A,X),(R_EAL r) by A4, TARSKI:def 3;
A13: less_eq_dom (chi A,X),(R_EAL r) = X by A12, XBOOLE_0:def 10;
A14: less_eq_dom (chi A,X),(R_EAL r) in S by A13, PROB_1:11;
thus B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by A14, FINSUB_1:def 2; :: thesis: verum
end;
suppose A15: ( 0 <= r & r < 1 ) ; :: thesis: B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S
A16: 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 A17: x in less_eq_dom (chi A,X),(R_EAL r) ; :: thesis: x in X \ A
reconsider x = x as Element of X by A17;
A18: (chi A,X) . x <= R_EAL r by A17, MESFUNC1:def 13;
A19: not x in A by A15, A18, FUNCT_3:def 3;
thus x in X \ A by A19, XBOOLE_0:def 5; :: thesis: verum
end;
A20: less_eq_dom (chi A,X),(R_EAL r) c= X \ A by A16, TARSKI:def 3;
A21: 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 A22: x in X \ A ; :: thesis: x in less_eq_dom (chi A,X),(R_EAL r)
A23: x in X by A22;
A24: not x in A by A22, XBOOLE_0:def 5;
reconsider x = x as Element of X by A22;
A25: (chi A,X) . x = 0. by A24, FUNCT_3:def 3;
A26: x in dom (chi A,X) by A23, FUNCT_3:def 3;
thus x in less_eq_dom (chi A,X),(R_EAL r) by A15, A25, A26, MESFUNC1:def 13; :: thesis: verum
end;
A27: X \ A c= less_eq_dom (chi A,X),(R_EAL r) by A21, TARSKI:def 3;
A28: less_eq_dom (chi A,X),(R_EAL r) = X \ A by A20, A27, XBOOLE_0:def 10;
A29: X in S by PROB_1:11;
A30: less_eq_dom (chi A,X),(R_EAL r) in S by A28, A29, MEASURE1:20;
thus B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by A30, FINSUB_1:def 2; :: thesis: verum
end;
suppose A31: r < 0 ; :: thesis: B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S
A32: for x being Element of X holds not x in less_eq_dom (chi A,X),(R_EAL r)
proof
assume A33: ex x being Element of X st x in less_eq_dom (chi A,X),(R_EAL r) ; :: thesis: contradiction
consider x being Element of X such that
A34: x in less_eq_dom (chi A,X),(R_EAL r) by A33;
A35: 0. <= (chi A,X) . x
proof
A36: now
per cases ( x in A or not x in A ) ;
suppose A37: x in A ; :: thesis: 0. <= (chi A,X) . x
thus 0. <= (chi A,X) . x by A37, FUNCT_3:def 3; :: thesis: verum
end;
end;
end;
thus 0. <= (chi A,X) . x by A36; :: thesis: verum
end;
thus contradiction by A31, A34, A35, MESFUNC1:def 13; :: thesis: verum
end;
A39: less_eq_dom (chi A,X),(R_EAL r) = {} by A32, SUBSET_1:10;
thus B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by A39, PROB_1:10; :: thesis: verum
end;
end;
end;
thus B /\ (less_eq_dom (chi A,X),(R_EAL r)) in S by A2; :: thesis: verum
end;
thus chi A,X is_measurable_on B by A1, MESFUNC1:32; :: thesis: verum