let X be non empty set ; for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for F being Function of RAT,S
for r being Real
for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let S be SigmaField of X; for f, g being PartFunc of X,ExtREAL
for F being Function of RAT,S
for r being Real
for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let f, g be PartFunc of X,ExtREAL; for F being Function of RAT,S
for r being Real
for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let F be Function of RAT,S; for r being Real
for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let r be Real; for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let A be Element of S; ( f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) implies A /\ (less_dom ((f + g),r)) = union (rng F) )
assume that
A1:
f is ()
and
A2:
g is ()
and
A3:
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
; A /\ (less_dom ((f + g),r)) = union (rng F)
A4:
dom (f + g) = (dom f) /\ (dom g)
by A1, A2, Th16;
A5:
union (rng F) c= A /\ (less_dom ((f + g),r))
proof
let x be
object ;
TARSKI:def 3 ( not x in union (rng F) or x in A /\ (less_dom ((f + g),r)) )
assume
x in union (rng F)
;
x in A /\ (less_dom ((f + g),r))
then consider Y being
set such that A6:
x in Y
and A7:
Y in rng F
by TARSKI:def 4;
consider p being
object such that A8:
p in dom F
and A9:
Y = F . p
by A7, FUNCT_1:def 3;
reconsider p =
p as
Rational by A8;
A10:
x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
by A3, A6, A9;
then A11:
x in A /\ (less_dom (f,p))
by XBOOLE_0:def 4;
then A12:
x in A
by XBOOLE_0:def 4;
A13:
x in less_dom (
f,
p)
by A11, XBOOLE_0:def 4;
x in A /\ (less_dom (g,(r - p)))
by A10, XBOOLE_0:def 4;
then A14:
x in less_dom (
g,
(r - p))
by XBOOLE_0:def 4;
reconsider x =
x as
Element of
X by A10;
f . x < p
by A13, MESFUNC1:def 11;
then A15:
f . x <> +infty
by XXREAL_0:4;
A16:
-infty < f . x
by A1;
A17:
-infty < g . x
by A2;
A18:
g . x < r - p
by A14, MESFUNC1:def 11;
then
g . x <> +infty
by XXREAL_0:4;
then reconsider f1 =
f . x,
g1 =
g . x as
Element of
REAL by A16, A17, A15, XXREAL_0:14;
A19:
p < r - g1
by A18, XREAL_1:12;
f1 < p
by A13, MESFUNC1:def 11;
then
f1 < r - g1
by A19, XXREAL_0:2;
then A20:
f1 + g1 < r
by XREAL_1:20;
A21:
x in dom g
by A14, MESFUNC1:def 11;
x in dom f
by A13, MESFUNC1:def 11;
then A22:
x in dom (f + g)
by A4, A21, XBOOLE_0:def 4;
then (f + g) . x =
(f . x) + (g . x)
by MESFUNC1:def 3
.=
f1 + g1
by SUPINF_2:1
;
then
x in less_dom (
(f + g),
r)
by A20, A22, MESFUNC1:def 11;
hence
x in A /\ (less_dom ((f + g),r))
by A12, XBOOLE_0:def 4;
verum
end;
A /\ (less_dom ((f + g),r)) c= union (rng F)
proof
let x be
object ;
TARSKI:def 3 ( not x in A /\ (less_dom ((f + g),r)) or x in union (rng F) )
assume A23:
x in A /\ (less_dom ((f + g),r))
;
x in union (rng F)
then A24:
x in A
by XBOOLE_0:def 4;
A25:
x in less_dom (
(f + g),
r)
by A23, XBOOLE_0:def 4;
then A26:
x in dom (f + g)
by MESFUNC1:def 11;
then A27:
x in dom f
by A4, XBOOLE_0:def 4;
A28:
(f + g) . x < r
by A25, MESFUNC1:def 11;
A29:
x in dom g
by A4, A26, XBOOLE_0:def 4;
reconsider x =
x as
Element of
X by A23;
A30:
-infty < f . x
by A1;
A31:
(f . x) + (g . x) < r
by A26, A28, MESFUNC1:def 3;
then A32:
g . x <> +infty
by A30, XXREAL_3:52;
A33:
-infty < g . x
by A2;
then
f . x <> +infty
by A31, XXREAL_3:52;
then reconsider f1 =
f . x,
g1 =
g . x as
Element of
REAL by A30, A33, A32, XXREAL_0:14;
f . x < r - (g . x)
by A31, A30, A33, XXREAL_3:52;
then consider p being
Rational such that A34:
f1 < p
and A35:
p < r - g1
by RAT_1:7;
not
r - p <= g1
by A35, XREAL_1:12;
then
x in less_dom (
g,
(r - p))
by A29, MESFUNC1:def 11;
then A36:
x in A /\ (less_dom (g,(r - p)))
by A24, XBOOLE_0:def 4;
p in RAT
by RAT_1:def 2;
then
p in dom F
by FUNCT_2:def 1;
then A37:
F . p in rng F
by FUNCT_1:def 3;
x in less_dom (
f,
p)
by A27, A34, MESFUNC1:def 11;
then
x in A /\ (less_dom (f,p))
by A24, XBOOLE_0:def 4;
then
x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
by A36, XBOOLE_0:def 4;
then
x in F . p
by A3;
hence
x in union (rng F)
by A37, TARSKI:def 4;
verum
end;
hence
A /\ (less_dom ((f + g),r)) = union (rng F)
by A5; verum