let X be set ; for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal st A c= dom f holds
A /\ (great_eq_dom f,a) = A \ (A /\ (less_dom f,a))
let f be PartFunc of X,ExtREAL ; for A being set
for a being R_eal st A c= dom f holds
A /\ (great_eq_dom f,a) = A \ (A /\ (less_dom f,a))
let A be set ; for a being R_eal st A c= dom f holds
A /\ (great_eq_dom f,a) = A \ (A /\ (less_dom f,a))
let a be R_eal; ( A c= dom f implies A /\ (great_eq_dom f,a) = A \ (A /\ (less_dom f,a)) )
assume A1:
A c= dom f
; A /\ (great_eq_dom f,a) = A \ (A /\ (less_dom f,a))
dom f c= X
by RELAT_1:def 18;
then A3:
A c= X
by A1, XBOOLE_1:1;
for x being set st x in A /\ (great_eq_dom f,a) holds
x in A \ (A /\ (less_dom f,a))
proof
let x be
set ;
( x in A /\ (great_eq_dom f,a) implies x in A \ (A /\ (less_dom f,a)) )
assume A5:
x in A /\ (great_eq_dom f,a)
;
x in A \ (A /\ (less_dom f,a))
then A6:
x in A
by XBOOLE_0:def 4;
x in great_eq_dom f,
a
by A5, XBOOLE_0:def 4;
then
a <= f . x
by Def15;
then
not
x in less_dom f,
a
by Def12;
then
not
x in A /\ (less_dom f,a)
by XBOOLE_0:def 4;
hence
x in A \ (A /\ (less_dom f,a))
by A6, XBOOLE_0:def 5;
verum
end;
then A11:
A /\ (great_eq_dom f,a) c= A \ (A /\ (less_dom f,a))
by TARSKI:def 3;
for x being set st x in A \ (A /\ (less_dom f,a)) holds
x in A /\ (great_eq_dom f,a)
proof
let x be
set ;
( x in A \ (A /\ (less_dom f,a)) implies x in A /\ (great_eq_dom f,a) )
assume A13:
x in A \ (A /\ (less_dom f,a))
;
x in A /\ (great_eq_dom f,a)
then A14:
x in A
;
not
x in A /\ (less_dom f,a)
by A13, XBOOLE_0:def 5;
then A16:
not
x in less_dom f,
a
by A13, XBOOLE_0:def 4;
reconsider x =
x as
Element of
X by A3, A14;
reconsider y =
f . x as
R_eal ;
not
y < a
by A1, A14, A16, Def12;
then
x in great_eq_dom f,
a
by A1, A14, Def15;
hence
x in A /\ (great_eq_dom f,a)
by A13, XBOOLE_0:def 4;
verum
end;
then
A \ (A /\ (less_dom f,a)) c= A /\ (great_eq_dom f,a)
by TARSKI:def 3;
hence
A /\ (great_eq_dom f,a) = A \ (A /\ (less_dom f,a))
by A11, XBOOLE_0:def 10; verum