let X be set ; for f being PartFunc of X,ExtREAL
for A being set
for a being ExtReal 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 ExtReal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let A be set ; for a being ExtReal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let a be ExtReal; A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
for x being object 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
object ;
( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) )
assume A1:
x in A /\ (eq_dom (f,a))
;
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
then A2:
x in A
by XBOOLE_0:def 4;
A3:
x in eq_dom (
f,
a)
by A1, XBOOLE_0:def 4;
then A4:
a = f . x
by Def15;
reconsider x =
x as
Element of
X by A1;
A5:
x in dom f
by A3, Def15;
then
x in great_eq_dom (
f,
a)
by A4, Def14;
then A6:
x in A /\ (great_eq_dom (f,a))
by A2, XBOOLE_0:def 4;
x in less_eq_dom (
f,
a)
by A4, A5, Def12;
hence
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
by A6, XBOOLE_0:def 4;
verum
end;
then A7:
A /\ (eq_dom (f,a)) c= (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
;
for x being object 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
object ;
( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) )
assume A8:
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
;
x in A /\ (eq_dom (f,a))
then A9:
x in A /\ (great_eq_dom (f,a))
by XBOOLE_0:def 4;
A10:
x in less_eq_dom (
f,
a)
by A8, XBOOLE_0:def 4;
A11:
x in A
by A9, XBOOLE_0:def 4;
x in great_eq_dom (
f,
a)
by A9, XBOOLE_0:def 4;
then A12:
a <= f . x
by Def14;
A13:
f . x <= a
by A10, Def12;
reconsider x =
x as
Element of
X by A8;
A14:
x in dom f
by A10, Def12;
a = f . x
by A12, A13, XXREAL_0:1;
then
x in eq_dom (
f,
a)
by A14, Def15;
hence
x in A /\ (eq_dom (f,a))
by A11, XBOOLE_0:def 4;
verum
end;
then
(A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) c= A /\ (eq_dom (f,a))
;
hence
A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
by A7, XBOOLE_0:def 10; verum