:: WAYBEL21 semantic presentation

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

proof end;

end;

:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def 1 :

registration

let S, T be Semilattice;
cluster meet-preserving -> monotone M4(the carrier of S,the carrier of T);
coherence

proof end;

end;

registration

let S be Semilattice;
let T be upper-bounded Semilattice;
cluster -> meet-preserving SemilatticeHomomorphism of S,T;
coherence

proof end;

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 complete SubRelStr of T;
existence

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

proof end;

theorem :: WAYBEL21:22

proof end;

theorem :: WAYBEL21:23

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

proof end;

end;

:: deftheorem Def2 defines antitone WAYBEL21:def 2 :

registration

let T be non empty reflexive RelStr ;
let x be Element of T;
cluster {x} opp+id -> transitive directed monotone antitone ;
coherence

proof end;

end;

registration

let T be non empty reflexive RelStr ;
cluster reflexive strict monotone antitone NetStr of T;
existence

proof end;

end;

registration

let T be non empty RelStr ;
let F be non empty Subset of T;
cluster F opp+id -> antitone ;
coherence

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 of S;
cluster f * N -> antitone ;
coherence

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 of 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 of 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 by A1, YELLOW_6:def 12;

end;

:: deftheorem Def3 defines Embedding WAYBEL21:def 3 :

theorem Th36: :: WAYBEL21:36

for T being non empty 1-sorted
for N being net of T
for M being non empty 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 j' being Element of M st
( j' >= j & N . i >= M . j' ) ) 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 :

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;