let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
let M be sigma_Measure of S; :: thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M
let T be N_Measure_fam of S; :: thesis: ( ( for A being set st A in T holds
A is measure_zero of M ) implies meet T is measure_zero of M )
assume A1: for A being set st A in T holds
A is measure_zero of M ; :: thesis: meet T is measure_zero of M
ex A being set st
( A in T & A is measure_zero of M )
proof
consider F being sequence of (bool X) such that
A2: T = rng F by SUPINF_2:def 8;
take F . 0 ; :: thesis: ( F . 0 in T & F . 0 is measure_zero of M )
thus ( F . 0 in T & F . 0 is measure_zero of M ) by A1, A2, FUNCT_2:4; :: thesis: verum
end;
hence meet T is measure_zero of M by MEASURE1:36, SETFAM_1:3; :: thesis: verum