:: On The Topological Properties of Meet-Continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received December 20, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

::-------------------------------------------------------------------
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor A. Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------

registration

let L be non empty RelStr ;

cluster id L -> monotone ;

coherence
id L is monotone by YELLOW_2:11;

end;

definition

let S, T be non empty RelStr ;
let f be Function of S,T;

redefine attr f is antitone means :: WAYBEL_9:def 1
for x, y being Element of S st x <= y holds
f . x >= f . y;

compatibility
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y ) ;

end;

:: deftheorem defines antitone WAYBEL_9:def 1 :
for S, T being non empty RelStr
for f being Function of S,T holds
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y );

theorem Th1: :: WAYBEL_9:1

for S, T being RelStr
for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone

proof end;

theorem Th2: :: WAYBEL_9:2

for S, T being RelStr
for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone

proof end;

theorem :: WAYBEL_9:3

for A, B being 1-sorted
for F being Subset-Family of A
for G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds
G is Cover of B ;

Lm1: for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }

proof end;

theorem Th4: :: WAYBEL_9:4

for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds uparrow x = {x} "\/" ([#] L)

proof end;

Lm2: for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }

proof end;

theorem Th5: :: WAYBEL_9:5

for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds downarrow x = {x} "/\" ([#] L)

proof end;

theorem :: WAYBEL_9:6

for L being reflexive antisymmetric with_infima RelStr
for y being Element of L holds (y "/\") .: (uparrow y) = {y}

proof end;

theorem Th7: :: WAYBEL_9:7

for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds (x "/\") " {x} = uparrow x

proof end;

theorem Th8: :: WAYBEL_9:8

for T being non empty 1-sorted
for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N

proof end;

Lm3: for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L

proof end;

registration

let L be non empty reflexive RelStr ;
let D be non empty directed Subset of L;
let n be Function of D, the carrier of L;

cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> directed ;

coherence
NetStr(# D,( the InternalRel of L |_2 D),n #) is directed by WAYBEL_2:19;

end;

registration

let L be non empty reflexive transitive RelStr ;
let D be non empty directed Subset of L;
let n be Function of D, the carrier of L;

cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> transitive ;

coherence
NetStr(# D,( the InternalRel of L |_2 D),n #) is transitive by Lm3;

end;

:: cf WAYBEL_2:42

theorem Th9: :: WAYBEL_9:9

for L being non empty reflexive transitive RelStr st ( for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
L is satisfying_MC

proof end;

theorem Th10: :: WAYBEL_9:10

for L being non empty RelStr
for a being Element of L
for N being net of L holds a "/\" N is net of L

proof end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be net of L;

cluster x "/\" N -> transitive ;

coherence
x "/\" N is transitive by Th10;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty reflexive NetStr over L;

cluster x "/\" N -> reflexive ;

coherence
x "/\" N is reflexive

proof end;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty antisymmetric NetStr over L;

cluster x "/\" N -> antisymmetric ;

coherence
x "/\" N is antisymmetric

proof end;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty transitive NetStr over L;

cluster x "/\" N -> transitive ;

coherence
x "/\" N is transitive

proof end;

end;

registration

let L be non empty RelStr ;
let J be set ;
let f be Function of J, the carrier of L;

cluster FinSups f -> transitive ;

coherence
FinSups f is transitive

proof end;

end;

definition

let L be non empty RelStr ;
let N be NetStr over L;

func inf N -> Element of L equals :: WAYBEL_9:def 2
Inf ;

coherence
Inf is Element of L ;

end;

:: deftheorem defines inf WAYBEL_9:def 2 :
for L being non empty RelStr
for N being NetStr over L holds inf N = Inf ;

definition

let L be RelStr ;
let N be NetStr over L;

pred ex_sup_of N means :: WAYBEL_9:def 3
ex_sup_of rng the mapping of N,L;

pred ex_inf_of N means :: WAYBEL_9:def 4
ex_inf_of rng the mapping of N,L;

end;

:: deftheorem defines ex_sup_of WAYBEL_9:def 3 :
for L being RelStr
for N being NetStr over L holds
( ex_sup_of N iff ex_sup_of rng the mapping of N,L );

:: deftheorem defines ex_inf_of WAYBEL_9:def 4 :
for L being RelStr
for N being NetStr over L holds
( ex_inf_of N iff ex_inf_of rng the mapping of N,L );

definition

let L be RelStr ;

func L +id -> strict NetStr over L means :Def5: :: WAYBEL_9:def 5
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of it = id L );

existence
ex b₁ being strict NetStr over L st
( RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b₁ = id L )

proof end;

uniqueness
for b₁, b₂ being strict NetStr over L st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b₁ = id L & RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b₂ = id L holds
b₁ = b₂ ;

end;

:: deftheorem Def5 defines +id WAYBEL_9:def 5 :
for L being RelStr
for b₂ being strict NetStr over L holds
( b₂ = L +id iff ( RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b₂ = id L ) );

registration

let L be non empty RelStr ;

cluster L +id -> non empty strict ;

coherence
not L +id is empty

proof end;

end;

registration

let L be reflexive RelStr ;

cluster L +id -> reflexive strict ;

coherence
L +id is reflexive

proof end;

end;

registration

let L be antisymmetric RelStr ;

cluster L +id -> antisymmetric strict ;

coherence
L +id is antisymmetric

proof end;

end;

registration

let L be transitive RelStr ;

cluster L +id -> transitive strict ;

coherence
L +id is transitive

proof end;

end;

registration

let L be with_suprema RelStr ;

cluster L +id -> strict directed ;

coherence
L +id is directed

proof end;

end;

registration

let L be directed RelStr ;

cluster L +id -> strict directed ;

coherence
L +id is directed

proof end;

end;

registration

let L be non empty RelStr ;

cluster L +id -> strict monotone eventually-directed ;

coherence
( L +id is monotone & L +id is eventually-directed )

proof end;

end;

definition

let L be RelStr ;

func L opp+id -> strict NetStr over L means :Def6: :: WAYBEL_9:def 6
( the carrier of it = the carrier of L & the InternalRel of it = the InternalRel of L ~ & the mapping of it = id L );

existence
ex b₁ being strict NetStr over L st
( the carrier of b₁ = the carrier of L & the InternalRel of b₁ = the InternalRel of L ~ & the mapping of b₁ = id L )

proof end;

uniqueness
for b₁, b₂ being strict NetStr over L st the carrier of b₁ = the carrier of L & the InternalRel of b₁ = the InternalRel of L ~ & the mapping of b₁ = id L & the carrier of b₂ = the carrier of L & the InternalRel of b₂ = the InternalRel of L ~ & the mapping of b₂ = id L holds
b₁ = b₂ ;

end;

:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :
for L being RelStr
for b₂ being strict NetStr over L holds
( b₂ = L opp+id iff ( the carrier of b₂ = the carrier of L & the InternalRel of b₂ = the InternalRel of L ~ & the mapping of b₂ = id L ) );

theorem Th11: :: WAYBEL_9:11

for L being RelStr holds RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #)

proof end;

registration

let L be non empty RelStr ;

cluster L opp+id -> non empty strict ;

coherence
not L opp+id is empty

proof end;

end;

registration

let L be reflexive RelStr ;

cluster L opp+id -> reflexive strict ;

coherence
L opp+id is reflexive

proof end;

end;

registration

let L be antisymmetric RelStr ;

cluster L opp+id -> antisymmetric strict ;

coherence
L opp+id is antisymmetric

proof end;

end;

registration

let L be transitive RelStr ;

cluster L opp+id -> transitive strict ;

coherence
L opp+id is transitive

proof end;

end;

registration

let L be with_infima RelStr ;

cluster L opp+id -> strict directed ;

coherence
L opp+id is directed

proof end;

end;

registration

let L be non empty RelStr ;

cluster L opp+id -> strict antitone eventually-filtered ;

coherence
( L opp+id is antitone & L opp+id is eventually-filtered )

proof end;

end;

definition

let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let i be Element of N;

func N | i -> strict NetStr over L means :Def7: :: WAYBEL_9:def 7
( ( for x being object holds
( x in the carrier of it iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of it = the InternalRel of N |_2 the carrier of it & the mapping of it = the mapping of N | the carrier of it );

existence
ex b₁ being strict NetStr over L st
( ( for x being object holds
( x in the carrier of b₁ iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b₁ = the InternalRel of N |_2 the carrier of b₁ & the mapping of b₁ = the mapping of N | the carrier of b₁ )

proof end;

uniqueness
for b₁, b₂ being strict NetStr over L st ( for x being object holds
( x in the carrier of b₁ iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b₁ = the InternalRel of N |_2 the carrier of b₁ & the mapping of b₁ = the mapping of N | the carrier of b₁ & ( for x being object holds
( x in the carrier of b₂ iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b₂ = the InternalRel of N |_2 the carrier of b₂ & the mapping of b₂ = the mapping of N | the carrier of b₂ holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines | WAYBEL_9:def 7 :
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N
for b₄ being strict NetStr over L holds
( b₄ = N | i iff ( ( for x being object holds
( x in the carrier of b₄ iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b₄ = the InternalRel of N |_2 the carrier of b₄ & the mapping of b₄ = the mapping of N | the carrier of b₄ ) );

theorem :: WAYBEL_9:12

for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }

proof end;

theorem Th13: :: WAYBEL_9:13

for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) c= the carrier of N

proof end;

theorem Th14: :: WAYBEL_9:14

for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds N | i is full SubNetStr of N

proof end;

registration

let L be non empty 1-sorted ;
let N be non empty reflexive NetStr over L;
let i be Element of N;

cluster N | i -> non empty reflexive strict ;

coherence
( not N | i is empty & N | i is reflexive )

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty directed NetStr over L;
let i be Element of N;

cluster N | i -> non empty strict ;

coherence
not N | i is empty

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty reflexive antisymmetric NetStr over L;
let i be Element of N;

cluster N | i -> antisymmetric strict ;

coherence
N | i is antisymmetric

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty antisymmetric directed NetStr over L;
let i be Element of N;

cluster N | i -> antisymmetric strict ;

coherence
N | i is antisymmetric

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty reflexive transitive NetStr over L;
let i be Element of N;

cluster N | i -> transitive strict ;

coherence
N | i is transitive

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;

cluster N | i -> transitive strict directed ;

coherence
( N | i is transitive & N | i is directed )

proof end;

end;

theorem :: WAYBEL_9:15

for L being non empty 1-sorted
for N being non empty reflexive NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1

proof end;

theorem Th16: :: WAYBEL_9:16

for L being non empty 1-sorted
for N being non empty directed NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1

proof end;

theorem Th17: :: WAYBEL_9:17

for L being non empty 1-sorted
for N being net of L
for i being Element of N holds N | i is subnet of N

proof end;

registration

let T be non empty 1-sorted ;
let N be net of T;

cluster non empty transitive strict directed for subnet of N;

existence
ex b₁ being subnet of N st b₁ is strict

proof end;

end;

definition

let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
:: original: |
redefine func N | i -> strict subnet of N;
coherence
N | i is strict subnet of N by Th17;

end;

definition

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be NetStr over S;

func f * N -> strict NetStr over T means :Def8: :: WAYBEL_9:def 8
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = f * the mapping of N );

existence
ex b₁ being strict NetStr over T st
( RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₁ = f * the mapping of N )

proof end;

uniqueness
for b₁, b₂ being strict NetStr over T st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₁ = f * the mapping of N & RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₂ = f * the mapping of N holds
b₁ = b₂ ;

end;

:: deftheorem Def8 defines * WAYBEL_9:def 8 :
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T
for N being NetStr over S
for b₅ being strict NetStr over T holds
( b₅ = f * N iff ( RelStr(# the carrier of b₅, the InternalRel of b₅ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₅ = f * the mapping of N ) );

registration

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be non empty NetStr over S;

cluster f * N -> non empty strict ;

coherence
not f * N is empty

proof end;

end;

registration

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be reflexive NetStr over S;

cluster f * N -> reflexive strict ;

coherence
f * N is reflexive

proof end;

end;

registration

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be antisymmetric NetStr over S;

cluster f * N -> antisymmetric strict ;

coherence
f * N is antisymmetric

proof end;

end;

registration

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be transitive NetStr over S;

cluster f * N -> transitive strict ;

coherence
f * N is transitive

proof end;

end;

registration

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be directed NetStr over S;

cluster f * N -> strict directed ;

coherence
f * N is directed

proof end;

end;

theorem Th18: :: WAYBEL_9:18

for L being non empty RelStr
for N being non empty NetStr over L
for x being Element of L holds (x "/\") * N = x "/\" N

proof end;

theorem :: WAYBEL_9:19

for S, T being TopStruct
for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds
G is open

proof end;

theorem :: WAYBEL_9:20

for S, T being TopStruct
for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed

proof end;

definition

attr c₁ is strict ;
struct TopRelStr -> TopStruct , RelStr ;
aggr TopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;

end;

registration

let A be non empty set ;
let R be Relation of A,A;
let T be Subset-Family of A;

cluster TopRelStr(# A,R,T #) -> non empty ;

coherence
not TopRelStr(# A,R,T #) is empty ;

end;

registration

let x be set ;
let R be Relation of {x};
let T be Subset-Family of {x};

cluster TopRelStr(# {x},R,T #) -> 1 -element ;

coherence
TopRelStr(# {x},R,T #) is 1 -element ;

end;

registration

let X be set ;
let O be Order of X;
let T be Subset-Family of X;

cluster TopRelStr(# X,O,T #) -> reflexive transitive antisymmetric ;

coherence
( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric )

proof end;

end;

Lm4: for tau being Subset-Family of {0}
for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds
( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )

proof end;

registration

cluster finite 1 -element discrete reflexive strict for TopRelStr ;

existence
ex b₁ being TopRelStr st
( b₁ is reflexive & b₁ is discrete & b₁ is strict & b₁ is finite & b₁ is 1 -element )

proof end;

end;

definition

mode TopLattice is TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr ;

end;

registration

cluster non empty finite 1 -element TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict for TopRelStr ;

existence
ex b₁ being TopLattice st
( b₁ is strict & b₁ is discrete & b₁ is finite & b₁ is compact & b₁ is Hausdorff & b₁ is 1 -element )

proof end;

end;

registration

let T be non empty Hausdorff TopSpace;

cluster non empty -> non empty Hausdorff for SubSpace of T;

coherence
for b₁ being non empty SubSpace of T holds b₁ is Hausdorff ;

end;

theorem Th21: :: WAYBEL_9:21

for T being non empty TopSpace
for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p

proof end;

theorem Th22: :: WAYBEL_9:22

for T being non empty TopSpace
for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)

proof end;

theorem :: WAYBEL_9:23

for T being non empty TopSpace
for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)

proof end;

theorem Th24: :: WAYBEL_9:24

for T being non empty TopSpace
for p being Element of T
for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S

proof end;

theorem Th25: :: WAYBEL_9:25

for T being Hausdorff TopLattice
for N being convergent net of T
for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)

proof end;

theorem Th26: :: WAYBEL_9:26

for T being Hausdorff TopLattice
for N being convergent net of T
for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)

proof end;

theorem Th27: :: WAYBEL_9:27

for S being Hausdorff TopLattice
for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds
uparrow x is closed

proof end;

theorem Th28: :: WAYBEL_9:28

for S being Hausdorff compact TopLattice
for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds
downarrow x is closed

proof end;

definition

let T be non empty TopSpace;
let N be non empty NetStr over T;
let p be Point of T;

pred p is_a_cluster_point_of N means :: WAYBEL_9:def 9
for O being a_neighborhood of p holds N is_often_in O;

end;

:: deftheorem defines is_a_cluster_point_of WAYBEL_9:def 9 :
for T being non empty TopSpace
for N being non empty NetStr over T
for p being Point of T holds
( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O );

theorem :: WAYBEL_9:29

for L being non empty TopSpace
for N being net of L
for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N

proof end;

theorem Th30: :: WAYBEL_9:30

for T being non empty Hausdorff compact TopSpace
for N being net of T ex c being Point of T st c is_a_cluster_point_of N

proof end;

theorem Th31: :: WAYBEL_9:31

for L being non empty TopSpace
for N being net of L
for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N by YELLOW_6:18;

theorem Th32: :: WAYBEL_9:32

for T being non empty TopSpace
for N being net of T
for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M

proof end;

theorem Th33: :: WAYBEL_9:33

for L being non empty Hausdorff compact TopSpace
for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) holds
for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N

proof end;

theorem Th34: :: WAYBEL_9:34

for S being non empty TopSpace
for c being Point of S
for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A

proof end;

Lm5: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N

proof end;

Lm6: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b

proof end;

theorem Th35: :: WAYBEL_9:35

for S being Hausdorff compact TopLattice
for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N

proof end;

Lm7: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N

proof end;

Lm8: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b

proof end;

theorem Th36: :: WAYBEL_9:36

for S being Hausdorff compact TopLattice
for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N

proof end;

:: Proposition 4.4 s. 32 (i) & (ii) => MC

theorem Th37: :: WAYBEL_9:37

for S being Hausdorff TopLattice st ( 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 ) holds
S is meet-continuous

proof end;

:: Proposition 4.4 s. 32 (ii) => (i)

theorem Th38: :: WAYBEL_9:38

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N )

proof end;

:: Proposition 4.4 s. 32 (ii) => (i) dual

theorem Th39: :: WAYBEL_9:39

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N )

proof end;

theorem :: WAYBEL_9:40

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
S is bounded

proof end;

theorem :: WAYBEL_9:41

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
S is meet-continuous

proof end;