let X be set ; for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let f be PartFunc of X,ExtREAL ; for A being set
for a being R_eal holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let A be set ; for a being R_eal holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let a be R_eal; A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
for x being set st x in A /\ (eq_dom f,a) holds
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
proof
let x be
set ;
( x in A /\ (eq_dom f,a) implies x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) )
assume A2:
x in A /\ (eq_dom f,a)
;
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
then A3:
x in A
by XBOOLE_0:def 4;
A4:
x in eq_dom f,
a
by A2, XBOOLE_0:def 4;
then A5:
a = f . x
by Def16;
reconsider x =
x as
Element of
X by A2;
A6:
x in dom f
by A4, Def16;
then
x in great_eq_dom f,
a
by A5, Def15;
then A8:
x in A /\ (great_eq_dom f,a)
by A3, XBOOLE_0:def 4;
x in less_eq_dom f,
a
by A5, A6, Def13;
hence
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A8, XBOOLE_0:def 4;
verum
end;
then A10:
A /\ (eq_dom f,a) c= (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by TARSKI:def 3;
for x being set st x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) holds
x in A /\ (eq_dom f,a)
proof
let x be
set ;
( x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) implies x in A /\ (eq_dom f,a) )
assume A12:
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
;
x in A /\ (eq_dom f,a)
then A13:
x in A /\ (great_eq_dom f,a)
by XBOOLE_0:def 4;
A14:
x in less_eq_dom f,
a
by A12, XBOOLE_0:def 4;
A15:
x in A
by A13, XBOOLE_0:def 4;
x in great_eq_dom f,
a
by A13, XBOOLE_0:def 4;
then A17:
a <= f . x
by Def15;
A18:
f . x <= a
by A14, Def13;
reconsider x =
x as
Element of
X by A12;
A19:
x in dom f
by A14, Def13;
a = f . x
by A17, A18, XXREAL_0:1;
then
x in eq_dom f,
a
by A19, Def16;
hence
x in A /\ (eq_dom f,a)
by A15, XBOOLE_0:def 4;
verum
end;
then
(A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) c= A /\ (eq_dom f,a)
by TARSKI:def 3;
hence
A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A10, XBOOLE_0:def 10; verum