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)
A1:
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)
A3:
x in A
by A2, XBOOLE_0:def 4;
A4:
x in eq_dom f,
a
by A2, XBOOLE_0:def 4;
A5:
a = f . x
by A4, Def16;
reconsider x =
x as
Element of
X by A2;
A6:
x in dom f
by A4, Def16;
A7:
x in great_eq_dom f,
a
by A5, A6, Def15;
A8:
x in A /\ (great_eq_dom f,a)
by A3, A7, XBOOLE_0:def 4;
A9:
x in less_eq_dom f,
a
by A5, A6, Def13;
thus
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A8, A9, XBOOLE_0:def 4;
verum
end;
A10:
A /\ (eq_dom f,a) c= (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A1, TARSKI:def 3;
A11:
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)
A13:
x in A /\ (great_eq_dom f,a)
by A12, 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;
A16:
x in great_eq_dom f,
a
by A13, XBOOLE_0:def 4;
A17:
a <= f . x
by A16, 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;
A20:
a = f . x
by A17, A18, XXREAL_0:1;
A21:
x in eq_dom f,
a
by A19, A20, Def16;
thus
x in A /\ (eq_dom f,a)
by A15, A21, XBOOLE_0:def 4;
verum
end;
A22:
(A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) c= A /\ (eq_dom f,a)
by A11, TARSKI:def 3;
thus
A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A10, A22, XBOOLE_0:def 10; verum