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