let X be set ; for S being SigmaField of X
for F being Function of NAT ,S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom f,(R_EAL n)) ) holds
A /\ (eq_dom f,+infty ) = meet (rng F)
let S be SigmaField of X; for F being Function of NAT ,S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom f,(R_EAL n)) ) holds
A /\ (eq_dom f,+infty ) = meet (rng F)
let F be Function of NAT ,S; for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom f,(R_EAL n)) ) holds
A /\ (eq_dom f,+infty ) = meet (rng F)
let f be PartFunc of X,ExtREAL ; for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom f,(R_EAL n)) ) holds
A /\ (eq_dom f,+infty ) = meet (rng F)
let A be set ; ( ( for n being Element of NAT holds F . n = A /\ (great_dom f,(R_EAL n)) ) implies A /\ (eq_dom f,+infty ) = meet (rng F) )
assume A1:
for n being Element of NAT holds F . n = A /\ (great_dom f,(R_EAL n))
; A /\ (eq_dom f,+infty ) = meet (rng F)
A2:
for x being set st x in A /\ (eq_dom f,+infty ) holds
x in meet (rng F)
proof
let x be
set ;
( x in A /\ (eq_dom f,+infty ) implies x in meet (rng F) )
assume A3:
x in A /\ (eq_dom f,+infty )
;
x in meet (rng F)
A4:
x in A
by A3, XBOOLE_0:def 4;
A5:
x in eq_dom f,
+infty
by A3, XBOOLE_0:def 4;
A6:
for
Y being
set st
Y in rng F holds
x in Y
proof
let Y be
set ;
( Y in rng F implies x in Y )
A7:
(
Y in rng F implies
x in Y )
proof
assume A8:
Y in rng F
;
x in Y
consider m being
Element of
NAT such that
m in dom F
and A9:
Y = F . m
by A8, PARTFUN1:26;
A10:
Y = A /\ (great_dom f,(R_EAL m))
by A1, A9;
reconsider x =
x as
Element of
X by A3;
A11:
f . x = +infty
by A5, Def16;
A12:
(
x in dom f & not
+infty <= R_EAL m )
by A5, Def16, XXREAL_0:9;
A13:
x in great_dom f,
(R_EAL m)
by A11, A12, Def14;
thus
x in Y
by A4, A10, A13, XBOOLE_0:def 4;
verum
end;
thus
(
Y in rng F implies
x in Y )
by A7;
verum
end;
thus
x in meet (rng F)
by A6, SETFAM_1:def 1;
verum
end;
A14:
A /\ (eq_dom f,+infty ) c= meet (rng F)
by A2, TARSKI:def 3;
A15:
for x being set st x in meet (rng F) holds
x in A /\ (eq_dom f,+infty )
proof
let x be
set ;
( x in meet (rng F) implies x in A /\ (eq_dom f,+infty ) )
assume A16:
x in meet (rng F)
;
x in A /\ (eq_dom f,+infty )
A17:
for
m being
Element of
NAT holds
(
x in A &
x in dom f & ex
y being
R_eal st
(
y = f . x &
y = +infty ) )
proof
let m be
Element of
NAT ;
( x in A & x in dom f & ex y being R_eal st
( y = f . x & y = +infty ) )
A18:
m in NAT
;
A19:
m in dom F
by A18, FUNCT_2:def 1;
A20:
F . m in rng F
by A19, FUNCT_1:def 5;
A21:
x in F . m
by A16, A20, SETFAM_1:def 1;
A22:
x in A /\ (great_dom f,(R_EAL m))
by A1, A21;
A23:
x in great_dom f,
(R_EAL m)
by A22, XBOOLE_0:def 4;
A24:
for
r being
Real holds
R_EAL r < f . x
proof
let r be
Real;
R_EAL r < f . x
consider n being
Element of
NAT such that A25:
r <= n
by Th11;
A26:
n in NAT
;
A27:
n in dom F
by A26, FUNCT_2:def 1;
A28:
F . n in rng F
by A27, FUNCT_1:def 5;
A29:
x in F . n
by A16, A28, SETFAM_1:def 1;
A30:
x in A /\ (great_dom f,(R_EAL n))
by A1, A29;
A31:
x in great_dom f,
(R_EAL n)
by A30, XBOOLE_0:def 4;
A32:
R_EAL n < f . x
by A31, Def14;
thus
R_EAL r < f . x
by A25, A32, XXREAL_0:2;
verum
end;
A33:
f . x = +infty
by A24, Th15;
thus
(
x in A &
x in dom f & ex
y being
R_eal st
(
y = f . x &
y = +infty ) )
by A22, A23, A33, Def14, XBOOLE_0:def 4;
verum
end;
A34:
1
in NAT
;
A35:
1
in dom F
by A34, FUNCT_2:def 1;
A36:
F . 1
in rng F
by A35, FUNCT_1:def 5;
A37:
x in F . 1
by A16, A36, SETFAM_1:def 1;
A38:
x in A /\ (great_dom f,(R_EAL 1))
by A1, A37;
reconsider x =
x as
Element of
X by A38;
A39:
x in eq_dom f,
+infty
by A17, Def16;
thus
x in A /\ (eq_dom f,+infty )
by A17, A39, XBOOLE_0:def 4;
verum
end;
A40:
meet (rng F) c= A /\ (eq_dom f,+infty )
by A15, TARSKI:def 3;
thus
A /\ (eq_dom f,+infty ) = meet (rng F)
by A14, A40, XBOOLE_0:def 10; verum