let X be set ; for S being SigmaField of X
for F being sequence of 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,n)) ) holds
A /\ (less_dom (f,+infty)) = union (rng F)
let S be SigmaField of X; for F being sequence of 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,n)) ) holds
A /\ (less_dom (f,+infty)) = union (rng F)
let F be sequence of 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,n)) ) holds
A /\ (less_dom (f,+infty)) = union (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,n)) ) holds
A /\ (less_dom (f,+infty)) = union (rng F)
let A be set ; ( ( for n being Element of NAT holds F . n = A /\ (less_dom (f,n)) ) implies A /\ (less_dom (f,+infty)) = union (rng F) )
assume A1:
for n being Element of NAT holds F . n = A /\ (less_dom (f,n))
; A /\ (less_dom (f,+infty)) = union (rng F)
for x being object st x in A /\ (less_dom (f,+infty)) holds
x in union (rng F)
proof
let x be
object ;
( x in A /\ (less_dom (f,+infty)) implies x in union (rng F) )
assume A2:
x in A /\ (less_dom (f,+infty))
;
x in union (rng F)
then A3:
x in A
by XBOOLE_0:def 4;
A4:
x in less_dom (
f,
+infty)
by A2, XBOOLE_0:def 4;
then A5:
x in dom f
by Def11;
A6:
f . x < +infty
by A4, Def11;
ex
n being
Element of
NAT st
f . x < n
then consider n being
Element of
NAT such that A10:
f . x < n
;
reconsider x =
x as
Element of
X by A2;
x in less_dom (
f,
n)
by A5, A10, Def11;
then
x in A /\ (less_dom (f,n))
by A3, XBOOLE_0:def 4;
then A11:
x in F . n
by A1;
n in NAT
;
then
n in dom F
by FUNCT_2:def 1;
then
F . n in rng F
by FUNCT_1:def 3;
hence
x in union (rng F)
by A11, TARSKI:def 4;
verum
end;
then A12:
A /\ (less_dom (f,+infty)) c= union (rng F)
;
for x being object st x in union (rng F) holds
x in A /\ (less_dom (f,+infty))
proof
let x be
object ;
( x in union (rng F) implies x in A /\ (less_dom (f,+infty)) )
assume
x in union (rng F)
;
x in A /\ (less_dom (f,+infty))
then consider Y being
set such that A13:
x in Y
and A14:
Y in rng F
by TARSKI:def 4;
consider m being
Element of
NAT such that
m in dom F
and A15:
F . m = Y
by A14, PARTFUN1:3;
A16:
x in A /\ (less_dom (f,m))
by A1, A13, A15;
then A17:
x in A
by XBOOLE_0:def 4;
A18:
x in less_dom (
f,
m)
by A16, XBOOLE_0:def 4;
then A19:
x in dom f
by Def11;
A20:
f . x < m
by A18, Def11;
reconsider x =
x as
Element of
X by A13, A14;
m in REAL
by XREAL_0:def 1;
then
f . x < +infty
by A20, XXREAL_0:2, XXREAL_0:9;
then
x in less_dom (
f,
+infty)
by A19, Def11;
hence
x in A /\ (less_dom (f,+infty))
by A17, XBOOLE_0:def 4;
verum
end;
then
union (rng F) c= A /\ (less_dom (f,+infty))
;
hence
A /\ (less_dom (f,+infty)) = union (rng F)
by A12, XBOOLE_0:def 10; verum