let X be set ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
A1:
A /\ (eq_dom f,a) c= (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
proof
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 ;
:: thesis: ( 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)
;
:: thesis: x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
then A3:
(
x in A &
x in eq_dom f,
a )
by XBOOLE_0:def 4;
then A4:
a = f . x
by Def16;
reconsider x =
x as
Element of
X by A2;
A5:
x in dom f
by A3, Def16;
then
x in great_eq_dom f,
a
by A4, Def15;
then A6:
x in A /\ (great_eq_dom f,a)
by A3, XBOOLE_0:def 4;
x in less_eq_dom f,
a
by A4, A5, Def13;
hence
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A6, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
A /\ (eq_dom f,a) c= (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by TARSKI:def 3;
:: thesis: verum
end;
(A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) c= A /\ (eq_dom f,a)
proof
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 ;
:: thesis: ( x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) implies x in A /\ (eq_dom f,a) )
assume A7:
x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
;
:: thesis: x in A /\ (eq_dom f,a)
then A8:
(
x in A /\ (great_eq_dom f,a) &
x in less_eq_dom f,
a )
by XBOOLE_0:def 4;
then A9:
(
x in A &
x in great_eq_dom f,
a )
by XBOOLE_0:def 4;
then A10:
a <= f . x
by Def15;
A11:
f . x <= a
by A8, Def13;
reconsider x =
x as
Element of
X by A7;
A12:
x in dom f
by A8, Def13;
a = f . x
by A10, A11, XXREAL_0:1;
then
x in eq_dom f,
a
by A12, Def16;
hence
x in A /\ (eq_dom f,a)
by A9, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
(A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) c= A /\ (eq_dom f,a)
by TARSKI:def 3;
:: thesis: verum
end;
hence
A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
by A1, XBOOLE_0:def 10; :: thesis: verum