:: by Grzegorz Bancerek

::

:: Received July 12, 1998

:: Copyright (c) 1998-2018 Association of Mizar Users

definition

let S, T be Semilattice;

assume A1: ( S is upper-bounded implies T is upper-bounded ) ;

ex b_{1} being Function of S,T st

for X being finite Subset of S holds b_{1} preserves_inf_of X

end;
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 for X being finite Subset of S holds it preserves_inf_of X;

ex b

for X being finite Subset of S holds b

proof 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_{3} being Function of S,T holds

( b_{3} is SemilatticeHomomorphism of S,T iff for X being finite Subset of S holds b_{3} preserves_inf_of X );

for S, T being Semilattice st ( S is upper-bounded implies T is upper-bounded ) holds

for b

( b

registration

let S, T be Semilattice;

for b_{1} being Function of S,T st b_{1} is meet-preserving holds

b_{1} is monotone

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

coherence for b

b

proof end;

registration

let S be Semilattice;

let T be upper-bounded Semilattice;

coherence

for b_{1} being SemilatticeHomomorphism of S,T holds b_{1} is meet-preserving
by Def1;

end;
let T be upper-bounded Semilattice;

coherence

for b

theorem :: WAYBEL21:1

for S, T being upper-bounded Semilattice

for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T

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

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

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

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

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 ) )

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 ) )

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

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

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

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

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 ) )

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;

registration

let T be complete LATTICE;

ex b_{1} being CLSubFrame of T st b_{1} is complete

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

existence ex b

proof 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 )

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 )

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

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

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

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

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

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

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

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

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)

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;

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

N . i >= N . j )

end;
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 for i, j being Element of N st i <= j holds

N . i >= N . j;

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

N . i >= N . j )

proof 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 );

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;

coherence

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

end;
let x be Element of T;

coherence

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

proof end;

registration

let T be non empty reflexive RelStr ;

existence

ex b_{1} being net of T st

( b_{1} is monotone & b_{1} is antitone & b_{1} is reflexive & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let T be non empty RelStr ;

let F be non empty Subset of T;

coherence

F opp+id is antitone

end;
let F be non empty Subset of T;

coherence

F opp+id is antitone

proof 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;

coherence

f * N is antitone

end;
let f be monotone Function of S,T;

let N be non empty antitone NetStr over S;

coherence

f * N is antitone

proof 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

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

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

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

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)

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

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))

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 )

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)

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 )

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)

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 ;

ex b_{1} being Function of M,N st

( the mapping of M = the mapping of N * b_{1} & ( 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_{1} . p ) )
by A1, YELLOW_6:def 9;

end;
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 ( 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 ) );

ex b

( the mapping of M = the mapping of N * b

for p being Element of M st n <= p holds

m <= b

:: 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_{4} being Function of M,N holds

( b_{4} is Embedding of M,N iff ( the mapping of M = the mapping of N * b_{4} & ( 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_{4} . p ) ) );

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

( b

for p being Element of M st n <= p holds

m <= b

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)

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

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

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 )

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 )

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

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 )

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

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)}

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 ) ) )

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 ) )

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;

end;
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);

for N being net of S holds f . (lim_inf N) = lim_inf (f * N);

:: 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) );

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 )

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

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

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 )

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

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

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

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 )

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;