let L be complete LATTICE; :: thesis: ( L is continuous iff for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) )
set AR = L -waybelow ;
hereby :: thesis: ( ( for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) ) implies L is continuous )
assume A1:
L is
continuous
;
:: thesis: for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating )then reconsider L' =
L as
lower-bounded meet-continuous LATTICE ;
thus
for
R being
auxiliary approximating Relation of
L holds
(
L -waybelow c= R &
L -waybelow is
approximating )
:: thesis: verumproof
let R be
auxiliary approximating Relation of
L;
:: thesis: ( L -waybelow c= R & L -waybelow is approximating )
reconsider R' =
R as
auxiliary approximating Relation of
L' ;
for
a,
b being
set st
[a,b] in L -waybelow holds
[a,b] in R
proof
let a,
b be
set ;
:: thesis: ( [a,b] in L -waybelow implies [a,b] in R )
assume A2:
[a,b] in L -waybelow
;
:: thesis: [a,b] in R
then reconsider a' =
a,
b' =
b as
Element of
L' by ZFMISC_1:106;
a' << b'
by A2, Def2;
then A3:
a' in waybelow b'
by WAYBEL_3:7;
A4:
meet { (A1 -below b') where A1 is auxiliary Relation of L' : A1 in App L' } = waybelow b'
by Th44;
R' in App L'
by Def20;
then
R' -below b' in { (A1 -below b') where A1 is auxiliary Relation of L' : A1 in App L' }
;
then
waybelow b' c= R' -below b'
by A4, SETFAM_1:4;
hence
[a,b] in R
by A3, Th13;
:: thesis: verum
end;
hence
L -waybelow c= R
by RELAT_1:def 3;
:: thesis: L -waybelow is approximating
thus
L -waybelow is
approximating
by A1;
:: thesis: verum
end;
end;
assume A5:
for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating )
; :: thesis: L is continuous
for x being Element of L holds x = sup (waybelow x)
then A6:
L is satisfying_axiom_of_approximation
by WAYBEL_3:def 5;
thus
L is continuous
by A6; :: thesis: verum