let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds

M . (meet (rng F)) = inf (rng (M * F))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds

M . (meet (rng F)) = inf (rng (M * F))

let M be sigma_Measure of S; :: thesis: for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds

M . (meet (rng F)) = inf (rng (M * F))

let F be sequence of S; :: thesis: ( ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty implies M . (meet (rng F)) = inf (rng (M * F)) )

assume that

A1: for n being Nat holds F . (n + 1) c= F . n and

A2: M . (F . 0) < +infty ; :: thesis: M . (meet (rng F)) = inf (rng (M * F))

consider G being sequence of S such that

A3: ( G . 0 = {} & ( for n being Nat holds G . (n + 1) = (F . 0) \ (F . n) ) ) by MEASURE2:9;

A4: union (rng G) = (F . 0) \ (meet (rng F)) by A1, A3, Th4;

A5: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A1, A3, Th5;

A6: for A being Element of S st A = union (rng G) holds

M . (meet (rng F)) = (M . (F . 0)) - (M . A)

then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23;

then M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A6;

hence M . (meet (rng F)) = inf (rng (M * F)) by A1, A2, A3, Th11; :: thesis: verum

for M being sigma_Measure of S

for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds

M . (meet (rng F)) = inf (rng (M * F))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds

M . (meet (rng F)) = inf (rng (M * F))

let M be sigma_Measure of S; :: thesis: for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds

M . (meet (rng F)) = inf (rng (M * F))

let F be sequence of S; :: thesis: ( ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty implies M . (meet (rng F)) = inf (rng (M * F)) )

assume that

A1: for n being Nat holds F . (n + 1) c= F . n and

A2: M . (F . 0) < +infty ; :: thesis: M . (meet (rng F)) = inf (rng (M * F))

consider G being sequence of S such that

A3: ( G . 0 = {} & ( for n being Nat holds G . (n + 1) = (F . 0) \ (F . n) ) ) by MEASURE2:9;

A4: union (rng G) = (F . 0) \ (meet (rng F)) by A1, A3, Th4;

A5: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A1, A3, Th5;

A6: for A being Element of S st A = union (rng G) holds

M . (meet (rng F)) = (M . (F . 0)) - (M . A)

proof

for n being Nat holds G . n c= G . (n + 1)
by A1, A3, MEASURE2:13;
let A be Element of S; :: thesis: ( A = union (rng G) implies M . (meet (rng F)) = (M . (F . 0)) - (M . A) )

assume A7: A = union (rng G) ; :: thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . A)

M . ((F . 0) \ (meet (rng F))) <> +infty by A2, MEASURE1:31, XBOOLE_1:36;

then M . A < +infty by A4, A7, XXREAL_0:4;

hence M . (meet (rng F)) = (M . (F . 0)) - (M . A) by A4, A5, A7, MEASURE1:32, XBOOLE_1:36; :: thesis: verum

end;assume A7: A = union (rng G) ; :: thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . A)

M . ((F . 0) \ (meet (rng F))) <> +infty by A2, MEASURE1:31, XBOOLE_1:36;

then M . A < +infty by A4, A7, XXREAL_0:4;

hence M . (meet (rng F)) = (M . (F . 0)) - (M . A) by A4, A5, A7, MEASURE1:32, XBOOLE_1:36; :: thesis: verum

then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23;

then M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A6;

hence M . (meet (rng F)) = inf (rng (M * F)) by A1, A2, A3, Th11; :: thesis: verum