let X be non empty set ; for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let S be SigmaField of X; for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let F be SetSequence of S; for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let r be Real; ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )
set E = dom (f . 0);
assume A1:
for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r))
; meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
now for x being object st x in meet (rng F) holds
x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))let x be
object ;
( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )assume A2:
x in meet (rng F)
;
x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))then reconsider z =
x as
Element of
X ;
A3:
F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),r))
by A1;
F . 0 in rng F
by FUNCT_2:4;
then
x in F . 0
by A2, SETFAM_1:def 1;
then A4:
x in dom (f . 0)
by A3, XBOOLE_0:def 4;
then A5:
x in dom (inf f)
by Def3;
then
r is
LowerBound of
rng (f # z)
by XXREAL_2:def 2;
then
r <= inf (f # z)
by XXREAL_2:def 4;
then
r <= (inf f) . x
by A5, Def3;
then
x in great_eq_dom (
(inf f),
r)
by A5, MESFUNC1:def 14;
hence
x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
by A4, XBOOLE_0:def 4;
verum end;
then A8:
meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
;
now for x being object st x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) holds
x in meet (rng F)let x be
object ;
( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) implies x in meet (rng F) )assume A9:
x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
;
x in meet (rng F)then reconsider z =
x as
Element of
X ;
A10:
x in dom (f . 0)
by A9, XBOOLE_0:def 4;
x in great_eq_dom (
(inf f),
r)
by A9, XBOOLE_0:def 4;
then A11:
r <= (inf f) . z
by MESFUNC1:def 14;
now for y being set st y in rng F holds
x in ylet y be
set ;
( y in rng F implies x in y )assume
y in rng F
;
x in ythen consider n being
object such that A12:
n in NAT
and A13:
y = F . n
by FUNCT_2:11;
reconsider n =
n as
Element of
NAT by A12;
A14:
x in dom (f . n)
by A10, Def2;
x in dom (inf f)
by A10, Def3;
then A15:
(inf f) . z = inf (f # z)
by Def3;
A16:
x in dom (f . 0)
by A9, XBOOLE_0:def 4;
(f . n) . z = (f # z) . n
by MESFUNC5:def 13;
then
inf (f # z) <= (f . n) . z
by RINFSUP2:23;
then
r <= (f . n) . z
by A11, A15, XXREAL_0:2;
then A17:
x in great_eq_dom (
(f . n),
r)
by A14, MESFUNC1:def 14;
F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r))
by A1;
hence
x in y
by A13, A16, A17, XBOOLE_0:def 4;
verum end; hence
x in meet (rng F)
by SETFAM_1:def 1;
verum end;
then
(dom (f . 0)) /\ (great_eq_dom ((inf f),r)) c= meet (rng F)
;
hence
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
by A8, XBOOLE_0:def 10; verum