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))
A2:
dom f c= X
by RELAT_1:def 18;
A3:
A c= X
by A1, A2, 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))
A6:
x in A
by A5, XBOOLE_0:def 4;
A7:
x in less_eq_dom f,
a
by A5, XBOOLE_0:def 4;
A8:
f . x <= a
by A7, Def13;
A9:
not
x in great_dom f,
a
by A8, Def14;
A10:
not
x in A /\ (great_dom f,a)
by A9, XBOOLE_0:def 4;
thus
x in A \ (A /\ (great_dom f,a))
by A6, A10, XBOOLE_0:def 5;
verum
end;
A11:
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)
A13:
x in A
by A12;
A14:
not
x in A /\ (great_dom f,a)
by A12, XBOOLE_0:def 5;
A15:
not
x in great_dom f,
a
by A12, A14, XBOOLE_0:def 4;
reconsider x =
x as
Element of
X by A3, A13;
reconsider y =
f . x as
R_eal ;
A16:
not
a < y
by A1, A13, A15, Def14;
A17:
x in less_eq_dom f,
a
by A1, A13, A16, Def13;
thus
x in A /\ (less_eq_dom f,a)
by A12, A17, XBOOLE_0:def 4;
verum
end;
A18:
A \ (A /\ (great_dom f,a)) c= A /\ (less_eq_dom f,a)
by A11, TARSKI:def 3;
thus
A /\ (less_eq_dom f,a) = A \ (A /\ (great_dom f,a))
by A4, A18, XBOOLE_0:def 10; verum