:: Lawson Topology in Continuous Lattices
:: by Grzegorz Bancerek
::
:: Received July 12, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

definition

let S, T be Semilattice;
assume A1: ( S is upper-bounded implies T is upper-bounded ) ;

mode SemilatticeHomomorphism of S,T -> Function of S,T means :Def1: :: WAYBEL21:def 1
for X being finite Subset of S holds it preserves_inf_of X;

existence
ex b₁ being Function of S,T st
for X being finite Subset of S holds b₁ preserves_inf_of X

proof end;

end;

:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def 1 :
for S, T being Semilattice st ( S is upper-bounded implies T is upper-bounded ) holds
for b₃ being Function of S,T holds
( b₃ is SemilatticeHomomorphism of S,T iff for X being finite Subset of S holds b₃ preserves_inf_of X );

registration

let S, T be Semilattice;

cluster Function-like V29( the carrier of S, the carrier of T) meet-preserving -> monotone for Element of K22(K23( the carrier of S, the carrier of T));

coherence
for b₁ being Function of S,T st b₁ is meet-preserving holds
b₁ is monotone

proof end;

end;

registration

let S be Semilattice;
let T be upper-bounded Semilattice;

cluster -> meet-preserving for SemilatticeHomomorphism of S,T;

coherence
for b₁ being SemilatticeHomomorphism of S,T holds b₁ is meet-preserving by Def1;

end;

theorem :: WAYBEL21:1

for S, T being upper-bounded Semilattice
for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T

proof end;

theorem Th2: :: WAYBEL21:2

for S, T being Semilattice
for f being Function of S,T st f is meet-preserving holds
for X being non empty finite Subset of S holds f preserves_inf_of X

proof end;

theorem :: WAYBEL21:3

for S, T being upper-bounded Semilattice
for f being meet-preserving Function of S,T st f . (Top S) = Top T holds
f is SemilatticeHomomorphism of S,T

proof end;

theorem Th4: :: WAYBEL21:4

for S, T being Semilattice
for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
for X being non empty Subset of S holds f preserves_inf_of X

proof end;

theorem Th5: :: WAYBEL21:5

for S, T being Semilattice
for f being Function of S,T st f is infs-preserving holds
f is SemilatticeHomomorphism of S,T

proof end;

theorem Th6: :: WAYBEL21:6

for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )

proof end;

theorem :: WAYBEL21:7

for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )

proof end;

theorem Th8: :: WAYBEL21:8

for T being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving

proof end;

theorem :: WAYBEL21:9

for T being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of T holds incl (S,T) is sups-preserving

proof end;

theorem Th10: :: WAYBEL21:10

for T being non empty up-complete Poset
for S being non empty full directed-sups-inheriting SubRelStr of T holds incl (S,T) is directed-sups-preserving

proof end;

theorem :: WAYBEL21:11

for T being complete LATTICE
for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving

proof end;

theorem Th12: :: WAYBEL21:12

for T1, T2, R being RelStr
for S being SubRelStr of T1 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds
( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )

proof end;

theorem Th13: :: WAYBEL21:13

for T being non empty RelStr holds T is full infs-inheriting sups-inheriting SubRelStr of T

proof end;

registration

let T be complete LATTICE;

cluster non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting with_infima complete for SubRelStr of T;

existence
ex b₁ being CLSubFrame of T st b₁ is complete

proof end;

end;

theorem Th14: :: WAYBEL21:14

for T being Semilattice
for S being non empty full SubRelStr of T holds
( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )

proof end;

theorem Th15: :: WAYBEL21:15

for T being sup-Semilattice
for S being non empty full SubRelStr of T holds
( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )

proof end;

theorem Th16: :: WAYBEL21:16

for T being upper-bounded Semilattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds
S is infs-inheriting

proof end;

theorem :: WAYBEL21:17

for T being lower-bounded sup-Semilattice
for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds
S is sups-inheriting

proof end;

theorem Th18: :: WAYBEL21:18

for T being complete LATTICE
for S being non empty full SubRelStr of T st S is infs-inheriting holds
S is complete

proof end;

theorem :: WAYBEL21:19

for T being complete LATTICE
for S being non empty full SubRelStr of T st S is sups-inheriting holds
S is complete

proof end;

theorem :: WAYBEL21:20

for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting

proof end;

theorem :: WAYBEL21:21

for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds
S2 is sups-inheriting

proof end;

theorem :: WAYBEL21:22

for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting

proof end;

theorem :: WAYBEL21:23

for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting

proof end;

theorem Th24: :: WAYBEL21:24

for S, T being non empty TopSpace
for N being net of S
for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)

proof end;

definition

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

redefine attr N is antitone means :Def2: :: WAYBEL21:def 2
for i, j being Element of N st i <= j holds
N . i >= N . j;

compatibility
( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j )

proof end;

end;

:: deftheorem Def2 defines antitone WAYBEL21:def 2 :
for T being non empty RelStr
for N being non empty NetStr over T holds
( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j );

registration

let T be non empty reflexive RelStr ;
let x be Element of T;

cluster {x} opp+id -> transitive directed monotone antitone ;

coherence
( {x} opp+id is transitive & {x} opp+id is directed & {x} opp+id is monotone & {x} opp+id is antitone )

proof end;

end;

registration

let T be non empty reflexive RelStr ;

cluster non empty reflexive transitive strict directed monotone antitone for NetStr over T;

existence
ex b₁ being net of T st
( b₁ is monotone & b₁ is antitone & b₁ is reflexive & b₁ is strict )

proof end;

end;

registration

let T be non empty RelStr ;
let F be non empty Subset of T;

cluster F opp+id -> antitone ;

coherence
F opp+id is antitone

proof end;

end;

registration

let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let N be non empty antitone NetStr over S;

cluster f * N -> antitone ;

coherence
f * N is antitone

proof end;

end;

theorem Th25: :: WAYBEL21:25

for S being complete LATTICE
for N being net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S

proof end;

theorem :: WAYBEL21:26

for S being non empty Poset
for N being reflexive monotone net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S

proof end;

theorem Th27: :: WAYBEL21:27

for S being non empty 1-sorted
for N being non empty NetStr over S
for X being set st rng the mapping of N c= X holds
N is_eventually_in X

proof end;

theorem Th28: :: WAYBEL21:28

for R being non empty /\-complete Poset
for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F

proof end;

theorem Th29: :: WAYBEL21:29

for S, T being non empty /\-complete Poset
for X being non empty filtered Subset of S
for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)

proof end;

theorem Th30: :: WAYBEL21:30

for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id

proof end;

theorem :: WAYBEL21:31

for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))

proof end;

theorem Th32: :: WAYBEL21:32

for S being non empty reflexive RelStr
for D being non empty Subset of S holds
( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )

proof end;

theorem Th33: :: WAYBEL21:33

for S, T being non empty up-complete Poset
for f being monotone Function of S,T
for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)

proof end;

theorem Th34: :: WAYBEL21:34

for S being non empty reflexive RelStr
for D being non empty directed Subset of S
for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )

proof end;

theorem Th35: :: WAYBEL21:35

for T being complete Lawson TopLattice
for D being non empty directed Subset of T holds sup D in Lim (Net-Str D)

proof end;

definition

let T be non empty 1-sorted ;
let N be net of T;
let M be non empty NetStr over T;
assume A1: M is subnet of N ;

mode Embedding of M,N -> Function of M,N means :Def3: :: WAYBEL21:def 3
( the mapping of M = the mapping of N * it & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= it . p ) );

existence
ex b₁ being Function of M,N st
( the mapping of M = the mapping of N * b₁ & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= b₁ . p ) ) by A1, YELLOW_6:def 9;

end;

:: deftheorem Def3 defines Embedding WAYBEL21:def 3 :
for T being non empty 1-sorted
for N being net of T
for M being non empty NetStr over T st M is subnet of N holds
for b₄ being Function of M,N holds
( b₄ is Embedding of M,N iff ( the mapping of M = the mapping of N * b₄ & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= b₄ . p ) ) );

theorem Th36: :: WAYBEL21:36

for T being non empty 1-sorted
for N being net of T
for M being subnet of N
for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)

proof end;

theorem Th37: :: WAYBEL21:37

for T being complete LATTICE
for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M

proof end;

theorem Th38: :: WAYBEL21:38

for T being complete LATTICE
for N being net of T
for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j & N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M

proof end;

theorem :: WAYBEL21:39

for T being non empty RelStr
for N being net of T
for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) holds
( M is subnet of N & incl (M,N) is Embedding of M,N )

proof end;

theorem Th40: :: WAYBEL21:40

for T being non empty RelStr
for N being net of T
for i being Element of N holds
( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )

proof end;

theorem Th41: :: WAYBEL21:41

for T being complete LATTICE
for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N

proof end;

theorem Th42: :: WAYBEL21:42

for T being non empty RelStr
for N being net of T
for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )

proof end;

theorem Th43: :: WAYBEL21:43

for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T

proof end;

theorem Th44: :: WAYBEL21:44

for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds Lim N = {(inf N)}

proof end;

theorem Th45: :: WAYBEL21:45

for S, T being complete Lawson TopLattice
for f being meet-preserving Function of S,T holds
( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )

proof end;

theorem Th46: :: WAYBEL21:46

for S, T being complete Lawson TopLattice
for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) )

proof end;

definition

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

attr f is lim_infs-preserving means :: WAYBEL21:def 4
for N being net of S holds f . (lim_inf N) = lim_inf (f * N);

end;

:: deftheorem defines lim_infs-preserving WAYBEL21:def 4 :
for S, T being non empty RelStr
for f being Function of S,T holds
( f is lim_infs-preserving iff for N being net of S holds f . (lim_inf N) = lim_inf (f * N) );

theorem :: WAYBEL21:47

for S, T being complete Lawson TopLattice
for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff f is lim_infs-preserving )

proof end;

theorem Th48: :: WAYBEL21:48

for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is infs-inheriting

proof end;

theorem Th49: :: WAYBEL21:49

for T being continuous complete Lawson TopLattice
for S being non empty full SubRelStr of T st ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is directed-sups-inheriting

proof end;

theorem Th50: :: WAYBEL21:50

for T being continuous complete Lawson TopLattice
for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st
( X = the carrier of S & X is closed )

proof end;

theorem Th51: :: WAYBEL21:51

for T being continuous complete Lawson TopLattice
for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T
for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S

proof end;

theorem Th52: :: WAYBEL21:52

for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is infs-inheriting

proof end;

theorem Th53: :: WAYBEL21:53

for T being continuous complete Lawson TopLattice
for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is directed-sups-inheriting

proof end;

theorem :: WAYBEL21:54

for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T
for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )

proof end;