let S be Hausdorff TopLattice; :: thesis: ( ( for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous )
assume that
A1:
for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N )
and
A2:
for x being Element of S holds x "/\" is continuous
; :: thesis: S is meet-continuous
for X being non empty directed Subset of S holds ex_sup_of X,S
proof
let X be non
empty directed Subset of
S;
:: thesis: ex_sup_of X,S
reconsider n =
id X as
Function of
X,the
carrier of
S by FUNCT_2:9;
set N =
NetStr(#
X,
(the InternalRel of S |_2 X),
n #);
NetStr(#
X,
(the InternalRel of S |_2 X),
n #) is
eventually-directed
by WAYBEL_2:20;
then A3:
ex_sup_of NetStr(#
X,
(the InternalRel of S |_2 X),
n #)
by A1;
rng the
mapping of
NetStr(#
X,
(the InternalRel of S |_2 X),
n #)
= X
by RELAT_1:71;
hence
ex_sup_of X,
S
by A3, Def3;
:: thesis: verum
end;
hence
S is up-complete
by WAYBEL_0:75; :: according to WAYBEL_2:def 7 :: thesis: S is satisfying_MC
for x being Element of S
for M being net of S st M is eventually-directed holds
x "/\" (sup M) = sup ({x} "/\" (rng (netmap M,S)))
proof
let x be
Element of
S;
:: thesis: for M being net of S st M is eventually-directed holds
x "/\" (sup M) = sup ({x} "/\" (rng (netmap M,S)))let M be
net of
S;
:: thesis: ( M is eventually-directed implies x "/\" (sup M) = sup ({x} "/\" (rng (netmap M,S))) )
assume A4:
M is
eventually-directed
;
:: thesis: x "/\" (sup M) = sup ({x} "/\" (rng (netmap M,S)))
set xM =
x "/\" M;
A5:
x "/\" M is
eventually-directed
by A4, WAYBEL_2:27;
A6:
x "/\" is
continuous
by A2;
A7:
sup M in Lim M
by A1, A4;
then reconsider M1 =
M as
convergent net of
S by YELLOW_6:def 19;
A8:
sup (x "/\" M) in Lim (x "/\" M)
by A1, A5;
then reconsider xM =
x "/\" M as
convergent net of
S by YELLOW_6:def 19;
A9:
x "/\" (lim M1) in Lim (x "/\" M1)
by A6, Th26;
thus x "/\" (sup M) =
x "/\" (lim M1)
by A7, YELLOW_6:def 20
.=
lim xM
by A9, YELLOW_6:def 20
.=
Sup
by A8, YELLOW_6:def 20
.=
sup (rng the mapping of xM)
by YELLOW_2:def 5
.=
sup ({x} "/\" (rng (netmap M,S)))
by WAYBEL_2:23
;
:: thesis: verum
end;
hence
S is satisfying_MC
by Th9; :: thesis: verum