let X be set ; for f being PartFunc of X,ExtREAL
for A being set
for a being ExtReal 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 ExtReal 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 ExtReal st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let a be ExtReal; ( 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 A2:
A c= X
by A1;
A3:
A /\ (less_eq_dom (f,a)) c= A \ (A /\ (great_dom (f,a)))
proof
let x be
object ;
TARSKI:def 3 ( not x in A /\ (less_eq_dom (f,a)) or x in A \ (A /\ (great_dom (f,a))) )
assume A4:
x in A /\ (less_eq_dom (f,a))
;
x in A \ (A /\ (great_dom (f,a)))
then A5:
x in A
by XBOOLE_0:def 4;
x in less_eq_dom (
f,
a)
by A4, XBOOLE_0:def 4;
then
f . x <= a
by Def12;
then
not
x in great_dom (
f,
a)
by Def13;
then
not
x in A /\ (great_dom (f,a))
by XBOOLE_0:def 4;
hence
x in A \ (A /\ (great_dom (f,a)))
by A5, XBOOLE_0:def 5;
verum
end;
for x being object st x in A \ (A /\ (great_dom (f,a))) holds
x in A /\ (less_eq_dom (f,a))
proof
let x be
object ;
( x in A \ (A /\ (great_dom (f,a))) implies x in A /\ (less_eq_dom (f,a)) )
assume A6:
x in A \ (A /\ (great_dom (f,a)))
;
x in A /\ (less_eq_dom (f,a))
then A7:
x in A
;
not
x in A /\ (great_dom (f,a))
by A6, XBOOLE_0:def 5;
then A8:
not
x in great_dom (
f,
a)
by A6, XBOOLE_0:def 4;
reconsider x =
x as
Element of
X by A2, A7;
reconsider y =
f . x as
R_eal ;
not
a < y
by A1, A7, A8, Def13;
then
x in less_eq_dom (
f,
a)
by A1, A7, Def12;
hence
x in A /\ (less_eq_dom (f,a))
by A6, XBOOLE_0:def 4;
verum
end;
then
A \ (A /\ (great_dom (f,a))) c= A /\ (less_eq_dom (f,a))
;
hence
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
by A3, XBOOLE_0:def 10; verum