let R be non empty up-complete /\-complete order_consistent TopLattice; :: thesis: for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let N be eventually-directed net of R; :: thesis: for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let x be Element of R; :: thesis: ( x <= lim_inf N iff x is_a_cluster_point_of N )
thus
( x <= lim_inf N implies x is_a_cluster_point_of N )
by Th33; :: thesis: ( x is_a_cluster_point_of N implies x <= lim_inf N )
thus
( x is_a_cluster_point_of N implies x <= lim_inf N )
:: thesis: verumproof
assume A1:
x is_a_cluster_point_of N
;
:: thesis: x <= lim_inf N
defpred S1[
Element of
N]
means verum;
deffunc H1(
Element of
N)
-> Element of the
carrier of
R =
"/\" { (N . i) where i is Element of N : i >= $1 } ,
R;
set X =
{ H1(j) where j is Element of N : S1[j] } ;
{ H1(j) where j is Element of N : S1[j] } is
Subset of
R
from DOMAIN_1:sch 8();
then reconsider D =
{ H1(j) where j is Element of N : S1[j] } as
Subset of
R ;
reconsider D =
D as non
empty directed Subset of
R by Th11;
for
G being
Subset of
R st
G is
open &
x in G holds
{(sup D)} meets G
proof
let G be
Subset of
R;
:: thesis: ( G is open & x in G implies {(sup D)} meets G )
assume A2:
G is
open
;
:: thesis: ( not x in G or {(sup D)} meets G )
assume
x in G
;
:: thesis: {(sup D)} meets G
then reconsider G =
G as
a_neighborhood of
x by A2, CONNSP_2:5;
A3:
N is_often_in G
by A1, WAYBEL_9:def 9;
now let i be
Element of
N;
:: thesis: sup D in Gconsider j1 being
Element of
N such that A4:
(
i <= j1 &
N . j1 in G )
by A3, WAYBEL_0:def 12;
consider j2 being
Element of
N such that A5:
for
k being
Element of
N st
j2 <= k holds
N . j1 <= N . k
by WAYBEL_0:11;
defpred S2[
Element of
N]
means $1
>= j2;
deffunc H2(
Element of
N)
-> Element of the
carrier of
R =
N . $1;
set E =
{ H2(k) where k is Element of N : S2[k] } ;
A6:
{ H2(k) where k is Element of N : S2[k] } is
Subset of
R
from DOMAIN_1:sch 8();
consider j' being
Element of
N such that A7:
(
j' >= j2 &
j' >= j2 )
by YELLOW_6:def 5;
N . j' in { H2(k) where k is Element of N : S2[k] }
by A7;
then reconsider E' =
{ H2(k) where k is Element of N : S2[k] } as non
empty Subset of
R by A6;
A8:
ex_inf_of E',
R
by WAYBEL_0:76;
N . j1 is_<=_than E'
then A12:
N . j1 <= "/\" E',
R
by A8, YELLOW_0:31;
for
a being
Element of
R holds
downarrow a = Cl {a}
by Def2;
then A13:
G is
upper
by A2, Th25;
then A14:
"/\" E',
R in G
by A4, A12, WAYBEL_0:def 20;
"/\" E',
R in D
;
then
"/\" E',
R <= sup D
by Th21;
hence
sup D in G
by A13, A14, WAYBEL_0:def 20;
:: thesis: verum end;
then
(
sup D in G &
sup D in {(sup D)} )
by TARSKI:def 1;
hence
{(sup D)} meets G
by XBOOLE_0:3;
:: thesis: verum
end;
then
x in Cl {(sup D)}
by PRE_TOPC:54;
then
x in downarrow (sup D)
by Def2;
hence
x <= lim_inf N
by WAYBEL_0:17;
:: thesis: verum
end;