let L be complete LATTICE; :: thesis: for D being non empty directed Subset of L
for M being subnet of Net-Str D holds lim_inf M = sup D
let D be non empty directed Subset of L; :: thesis: for M being subnet of Net-Str D holds lim_inf M = sup D
for M being subnet of Net-Str D holds sup D >= inf M
proof
let M be
subnet of
Net-Str D;
:: thesis: sup D >= inf M
consider i being
Element of
M;
set f = the
mapping of
M;
consider g being
Function of
M,
(Net-Str D) such that A1:
the
mapping of
M = the
mapping of
(Net-Str D) * g
and
for
m being
Element of
(Net-Str D) ex
n being
Element of
M st
for
p being
Element of
M st
n <= p holds
m <= g . p
by YELLOW_6:def 12;
A2:
dom the
mapping of
M = the
carrier of
M
by FUNCT_2:def 1;
g . i in the
carrier of
(Net-Str D)
;
then A3:
g . i in D
by WAYBEL21:32;
then g . i =
(id D) . (g . i)
by FUNCT_1:35
.=
the
mapping of
(Net-Str D) . (g . i)
by WAYBEL21:32
.=
the
mapping of
M . i
by A1, A2, FUNCT_1:22
;
then A4:
the
mapping of
M . i <= sup D
by A3, YELLOW_2:24;
A5:
ex_inf_of rng the
mapping of
M,
L
by YELLOW_0:17;
the
mapping of
M . i in rng the
mapping of
M
by A2, FUNCT_1:def 5;
then
"/\" (rng the mapping of M),
L <= the
mapping of
M . i
by A5, YELLOW_4:2;
then
sup D >= "/\" (rng the mapping of M),
L
by A4, YELLOW_0:def 2;
then
sup D >= Inf
by YELLOW_2:def 6;
hence
sup D >= inf M
by WAYBEL_9:def 2;
:: thesis: verum
end;
then
( lim_inf (Net-Str D) = sup D & ( for p being greater_or_equal_to_id Function of (Net-Str D),(Net-Str D) holds sup D >= inf ((Net-Str D) * p) ) )
by WAYBEL17:10;
hence
for M being subnet of Net-Str D holds lim_inf M = sup D
by Th15; :: thesis: verum