:: Lawson Topology in Continuous Lattices
:: by Grzegorz Bancerek
::
:: Received July 12, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies WAYBEL_0, LATTICES, FUNCT_1, FINSET_1, SUBSET_1, STRUCT_0,
FUNCOP_1, YELLOW_0, XBOOLE_0, RELAT_1, ORDINAL2, TARSKI, SEQM_3,
XXREAL_0, LATTICE3, ORDERS_2, REWRITE1, CAT_1, FUNCT_3, EQREL_1,
WELLORD1, WAYBEL_5, PRE_TOPC, ORDINAL1, CONNSP_2, TOPS_1, RCOMP_1,
RELAT_2, WAYBEL_9, ARYTM_0, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1,
YELLOW_9, PROB_1, YELLOW_2, PRELAMB, WAYBEL21;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, FINSET_1, TOLER_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1, ORDERS_2, LATTICE3, ORDERS_3,
YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3, WAYBEL_5, YELLOW_6, YELLOW_7,
WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL17, WAYBEL19;
constructors TOLER_1, TOPS_1, NATTRA_1, BORSUK_1, CANTOR_1, TOPS_2, ORDERS_3,
YELLOW_2, WAYBEL_3, WAYBEL17, YELLOW_9, WAYBEL19, COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, PRE_TOPC,
LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2, YELLOW_6, WAYBEL_9, WAYBEL10,
WAYBEL17, YELLOW_9, WAYBEL19, TOPS_1, RELSET_1;
requirements SUBSET, BOOLE;
begin :: Semilattice homomorphism and inheritance
definition
let S,T be Semilattice such that
S is upper-bounded implies T is upper-bounded;
mode SemilatticeHomomorphism of S,T -> Function of S,T means
:: WAYBEL21:def 1
for X being finite Subset of S holds it preserves_inf_of X;
end;
registration
let S,T be Semilattice;
cluster meet-preserving -> monotone for Function of S,T;
end;
registration
let S be Semilattice, T be upper-bounded Semilattice;
cluster -> meet-preserving for SemilatticeHomomorphism of S,T;
end;
theorem :: WAYBEL21:1
for S,T being upper-bounded Semilattice
for f being SemilatticeHomomorphism of S,T holds f.Top S = Top T;
theorem :: WAYBEL21:2
for S,T being Semilattice, f being Function of S,T st f is meet-preserving
for X being finite non empty Subset of S holds f preserves_inf_of X;
theorem :: WAYBEL21:3
for S,T being upper-bounded Semilattice, f being meet-preserving Function
of S, T st f.Top S = Top T holds f is SemilatticeHomomorphism of S,T;
theorem :: WAYBEL21:4
for S,T being Semilattice, f being Function of S,T st f is meet-preserving &
for X being filtered non empty Subset of S holds f preserves_inf_of X
for X being non empty Subset of S holds f preserves_inf_of X;
theorem :: WAYBEL21:5
for S,T being Semilattice, f being Function of S,T st f is infs-preserving
holds f is SemilatticeHomomorphism of S,T;
theorem :: WAYBEL21:6
for S1,T1,S2,T2 being non empty RelStr
st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
for f1 being Function of S1,T1, 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);
theorem :: WAYBEL21:7
for S1,T1,S2,T2 being non empty RelStr
st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
for f1 being Function of S1,T1, 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);
theorem :: WAYBEL21:8
for T being complete LATTICE
for S being infs-inheriting full non empty SubRelStr of T
holds incl(S,T) is infs-preserving;
theorem :: WAYBEL21:9
for T being complete LATTICE
for S being sups-inheriting full non empty SubRelStr of T
holds incl(S,T) is sups-preserving;
theorem :: WAYBEL21:10
for T being up-complete non empty Poset
for S being directed-sups-inheriting full non empty SubRelStr of T
holds incl(S,T) is directed-sups-preserving;
theorem :: WAYBEL21:11
for T being complete LATTICE
for S being filtered-infs-inheriting full non empty SubRelStr of T
holds incl(S,T) is filtered-infs-preserving;
theorem :: WAYBEL21:12
for T1,T2,R being RelStr, S being SubRelStr of T1
st the RelStr of T1 = the RelStr of T2 & the RelStr of S = the RelStr of R
holds R is SubRelStr of T2 & (S is full implies R is full SubRelStr of T2);
theorem :: WAYBEL21:13
for T being non empty RelStr holds
T is infs-inheriting sups-inheriting full SubRelStr of T;
registration
let T be complete LATTICE;
cluster complete for CLSubFrame of T;
end;
theorem :: WAYBEL21:14
for T being Semilattice for S being full non empty SubRelStr of T
holds S is meet-inheriting iff
for X being finite non empty Subset of S holds "/\"
(X, T) in the carrier of S;
theorem :: WAYBEL21:15
for T being sup-Semilattice for S being full non empty SubRelStr of T
holds S is join-inheriting iff
for X being finite non empty Subset of S holds "\/"
(X, T) in the carrier of S;
theorem :: WAYBEL21:16
for T being upper-bounded Semilattice
for S being meet-inheriting full non empty SubRelStr of T
st Top T in the carrier of S & S is filtered-infs-inheriting
holds S is infs-inheriting;
theorem :: WAYBEL21:17
for T being lower-bounded sup-Semilattice
for S being join-inheriting full non empty SubRelStr of T
st Bottom T in the carrier of S & S is directed-sups-inheriting
holds S is sups-inheriting;
theorem :: WAYBEL21:18
for T being complete LATTICE, S being full non empty SubRelStr of T
st S is infs-inheriting holds S is complete;
theorem :: WAYBEL21:19
for T being complete LATTICE, S being full non empty SubRelStr of T
st S is sups-inheriting holds S is complete;
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 the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is infs-inheriting implies S2 is infs-inheriting;
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 the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is sups-inheriting implies S2 is sups-inheriting;
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 the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting;
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 the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting;
begin :: Nets and limits
theorem :: WAYBEL21:24
for S,T being non empty TopSpace, N being net of S
for f being Function of S,T st f is continuous holds f.:Lim N c= Lim (f*N);
definition
let T be non empty RelStr;
let N be non empty NetStr over T;
redefine attr N is antitone means
:: WAYBEL21:def 2
for i,j being Element of N st i <= j holds N.i >= N.j;
end;
registration
let T be non empty reflexive RelStr;
let x be Element of T;
cluster {x} opp+id -> transitive directed monotone antitone;
end;
registration
let T be non empty reflexive RelStr;
cluster monotone antitone reflexive strict for net of T;
end;
registration
let T be non empty RelStr;
let F be non empty Subset of T;
cluster F opp+id -> antitone;
end;
registration
let S,T be non empty reflexive RelStr;
let f be monotone Function of S,T;
let N be antitone non empty NetStr over S;
cluster f*N -> antitone;
end;
theorem :: WAYBEL21:25
for S being complete LATTICE, N be net of S holds
the set of all "/\"({N.i where i is Element of N:i >= j},S)
where j is Element of N
is directed non empty Subset of S;
theorem :: WAYBEL21:26
for S being non empty Poset, N be monotone reflexive net of S holds
the set of all "/\"({N.i where i is Element of N: i >= j}, S)
where j is Element of N
is directed non empty Subset of S;
theorem :: WAYBEL21:27
for S being non empty 1-sorted, N being non empty NetStr over S, X being set
st rng the mapping of N c= X holds N is_eventually_in X;
theorem :: WAYBEL21:28
for R being /\-complete non empty Poset
for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F;
theorem :: WAYBEL21:29
for S,T being /\-complete non empty 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);
theorem :: 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;
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));
theorem :: WAYBEL21:32
for S being non empty reflexive RelStr, 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;
theorem :: WAYBEL21:33
for S,T being up-complete non empty 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);
theorem :: 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;
theorem :: WAYBEL21:35
for T being Lawson complete TopLattice
for D being directed non empty Subset of T holds sup D in Lim Net-Str D;
definition
let T be non empty 1-sorted;
let N be net of T, M be non empty NetStr over T such that
M is subnet of N;
mode Embedding of M,N -> Function of M,N means
:: 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;
end;
theorem :: WAYBEL21:36
for T being non empty 1-sorted for N being net of T, M being subnet of N
for e being Embedding of M,N, i being Element of M holds M.i = N.(e.i);
theorem :: WAYBEL21:37
for T being complete LATTICE for N being net of T, M being subnet of N
holds lim_inf N <= lim_inf M;
theorem :: WAYBEL21:38
for T being complete LATTICE for N being net of T, M being subnet of N
for e being Embedding of M, N
st for i being Element of N, j being Element of M st e.j <= i
ex j9 being Element of M st j9 >= j & N.i >= M.j9
holds lim_inf N = lim_inf M;
theorem :: WAYBEL21:39
for T being non empty RelStr
for N being net of T, 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;
theorem :: WAYBEL21:40
for T being non empty RelStr, 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;
theorem :: WAYBEL21:41
for T being complete LATTICE, N being net of T
for i being Element of N holds lim_inf (N|i) = lim_inf N;
theorem :: WAYBEL21:42
for T being non empty RelStr, N being net of T, X being set
st N is_eventually_in X
ex i be Element of N st N.i in X & rng the mapping of N|i c= X;
theorem :: WAYBEL21:43 :: see WAYBEL_2:18, for eventually-directed
for T being Lawson complete TopLattice
for N being eventually-filtered net of T
holds rng the mapping of N is filtered non empty Subset of T;
theorem :: WAYBEL21:44
:: 1.7. LEMMA, -- WAYBEL19:44 revised
for T being Lawson complete TopLattice
for N being eventually-filtered net of T holds Lim N = {inf N};
begin :: Lawson topology revisited
theorem :: WAYBEL21:45
:: 1.8. THEOREM, (1) <=> (2), generalized, p. 145
for S,T being Lawson complete 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;
theorem :: WAYBEL21:46
:: 1.8. THEOREM, (1) <=> (2), p. 145
for S,T being Lawson complete TopLattice
for f being SemilatticeHomomorphism of S,T holds
f is continuous iff f is infs-preserving directed-sups-preserving;
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;
theorem :: WAYBEL21:47
:: 1.8. THEOREM, (1) <=> (3), p. 145
for S,T being Lawson complete TopLattice
for f being SemilatticeHomomorphism of S,T holds
f is continuous iff f is lim_infs-preserving;
theorem :: WAYBEL21:48
:: 1.11. THEOREM, (1) => (2a), p. 147
for T being Lawson complete continuous TopLattice
for S being meet-inheriting full non empty 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;
theorem :: WAYBEL21:49
:: 1.11. THEOREM, (1) => (2b), p. 147
for T being Lawson complete continuous TopLattice
for S being full non empty 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;
theorem :: WAYBEL21:50
:: 1.11. THEOREM, (2) => (1), p. 147
for T being Lawson complete continuous TopLattice
for S being infs-inheriting directed-sups-inheriting full non empty
SubRelStr of T ex X being Subset of T st X = the carrier of S & X is closed;
theorem :: WAYBEL21:51
:: 1.11. THEOREM, (2) => (3+), p. 147
for T being Lawson complete continuous TopLattice
for S being infs-inheriting directed-sups-inheriting full non empty
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;
theorem :: WAYBEL21:52
:: 1.11. THEOREM, (3) => (2a), p. 147
for T being Lawson complete continuous TopLattice
for S being meet-inheriting full non empty 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;
theorem :: WAYBEL21:53
:: 1.11. THEOREM, (3) => (2b), p. 147
for T being Lawson complete continuous TopLattice
for S being full non empty 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;
theorem :: WAYBEL21:54
:: 1.11. THEOREM, (1) <=> (3+), p. 147
for T being Lawson complete continuous TopLattice
for S being meet-inheriting full non empty 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;