let T, T2 be complete lower TopLattice; :: thesis: ( T2 is TopAugmentation of [:T,T:] implies for f being Function of T2,T st f = inf_op T holds
f is continuous )
assume A1:
RelStr(# the carrier of T2,the InternalRel of T2 #) = RelStr(# the carrier of [:T,T:],the InternalRel of [:T,T:] #)
; :: according to YELLOW_9:def 4 :: thesis: for f being Function of T2,T st f = inf_op T holds
f is continuous
let f be Function of T2,T; :: thesis: ( f = inf_op T implies f is continuous )
assume A2:
f = inf_op T
; :: thesis: f is continuous
f is infs-preserving
proof
let X be
Subset of
T2;
:: according to WAYBEL_0:def 32 :: thesis: f preserves_inf_of X
reconsider Y =
X as
Subset of
[:T,T:] by A1;
assume A3:
ex_inf_of X,
T2
;
:: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,T2) )
then A4:
(
ex_inf_of Y,
[:T,T:] &
inf_op T preserves_inf_of Y )
by A1, WAYBEL_0:def 32, YELLOW_0:14;
thus
ex_inf_of f .: X,
T
by YELLOW_0:17;
:: thesis: "/\" (f .: X),T = f . ("/\" X,T2)
thus inf (f .: X) =
(inf_op T) . (inf Y)
by A2, A4, WAYBEL_0:def 30
.=
f . (inf X)
by A1, A2, A3, YELLOW_0:27
;
:: thesis: verum
end;
hence
f is continuous
by Th9; :: thesis: verum