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 /\ (less_eq_dom f,a) = A \ (A /\ (great_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 /\ (less_eq_dom f,a) = A \ (A /\ (great_dom f,a))
let A be set ; for a being R_eal st A c= dom f holds
A /\ (less_eq_dom f,a) = A \ (A /\ (great_dom f,a))
let a be R_eal; ( A c= dom f implies A /\ (less_eq_dom f,a) = A \ (A /\ (great_dom f,a)) )
assume A1:
A c= dom f
; A /\ (less_eq_dom f,a) = A \ (A /\ (great_dom f,a))
dom f c= X
by RELAT_1:def 18;
then A3:
A c= X
by A1, XBOOLE_1:1;
A4:
A /\ (less_eq_dom f,a) c= A \ (A /\ (great_dom f,a))
proof
let x be
set ;
TARSKI:def 3 ( not x in A /\ (less_eq_dom f,a) or x in A \ (A /\ (great_dom f,a)) )
assume A5:
x in A /\ (less_eq_dom f,a)
;
x in A \ (A /\ (great_dom f,a))
then A6:
x in A
by XBOOLE_0:def 4;
x in less_eq_dom f,
a
by A5, XBOOLE_0:def 4;
then
f . x <= a
by Def13;
then
not
x in great_dom f,
a
by Def14;
then
not
x in A /\ (great_dom f,a)
by XBOOLE_0:def 4;
hence
x in A \ (A /\ (great_dom f,a))
by A6, XBOOLE_0:def 5;
verum
end;
for x being set st x in A \ (A /\ (great_dom f,a)) holds
x in A /\ (less_eq_dom f,a)
proof
let x be
set ;
( x in A \ (A /\ (great_dom f,a)) implies x in A /\ (less_eq_dom f,a) )
assume A12:
x in A \ (A /\ (great_dom f,a))
;
x in A /\ (less_eq_dom f,a)
then A13:
x in A
;
not
x in A /\ (great_dom f,a)
by A12, XBOOLE_0:def 5;
then A15:
not
x in great_dom f,
a
by A12, XBOOLE_0:def 4;
reconsider x =
x as
Element of
X by A3, A13;
reconsider y =
f . x as
R_eal ;
not
a < y
by A1, A13, A15, Def14;
then
x in less_eq_dom f,
a
by A1, A13, Def13;
hence
x in A /\ (less_eq_dom f,a)
by A12, XBOOLE_0:def 4;
verum
end;
then
A \ (A /\ (great_dom f,a)) c= A /\ (less_eq_dom f,a)
by TARSKI:def 3;
hence
A /\ (less_eq_dom f,a) = A \ (A /\ (great_dom f,a))
by A4, XBOOLE_0:def 10; verum