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 /\ (less_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 /\ (less_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 /\ (less_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 /\ (less_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 /\ (less_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 /\ (less_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 /\ (less_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
R_EAL (- m) <= -infty )
by A5, Def16, XXREAL_0:12;
A13:
x in less_dom f,
(R_EAL (- m))
by A11, A12, Def12;
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 /\ (less_dom f,(R_EAL (- m)))
by A1, A21;
A23:
x in less_dom f,
(R_EAL (- m))
by A22, XBOOLE_0:def 4;
A24:
for
r being
Real holds
f . x < R_EAL r
proof
let r be
Real;
f . x < R_EAL r
consider n being
Element of
NAT such that A25:
- n <= r
by Th12;
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 /\ (less_dom f,(R_EAL (- n)))
by A1, A29;
A31:
x in less_dom f,
(R_EAL (- n))
by A30, XBOOLE_0:def 4;
A32:
f . x < R_EAL (- n)
by A31, Def12;
thus
f . x < R_EAL r
by A25, A32, XXREAL_0:2;
verum
end;
A33:
f . x = -infty
by A24, Th16;
thus
(
x in A &
x in dom f & ex
y being
R_eal st
(
y = f . x &
y = -infty ) )
by A22, A23, A33, Def12, 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 /\ (less_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