:: Meet Continuous Lattices Revisited
:: by Artur Korni{\l}owicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2016 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 XBOOLE_0, TARSKI, SUBSET_1, RELAT_2, ORDERS_2, WAYBEL_0,
YELLOW_1, CARD_FIL, STRUCT_0, ZFMISC_1, XXREAL_0, LATTICE3, ORDINAL2,
YELLOW_0, LATTICES, WAYBEL_2, YELLOW_9, WAYBEL11, REWRITE1, WAYBEL_9,
PRE_TOPC, PROB_1, WAYBEL19, PRELAMB, ORDINAL1, SETFAM_1, CANTOR_1, DIRAF,
RCOMP_1, FINSET_1, RLVECT_3, COMPTS_1, YELLOW_8, TOPS_1, WAYBEL29,
YELLOW13, FUNCT_1, WAYBEL21, RELAT_1, PARTFUN1, MCART_1, TOPS_2,
WAYBEL_3, TDLAT_3, CONNSP_2, EQREL_1, WAYBEL_8, WAYBEL_6, WAYBEL30,
CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, BINOP_1, FUNCT_3, SETFAM_1, DOMAIN_1, CARD_1, STRUCT_0,
FINSET_1, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2,
TDLAT_3, LATTICE3, BORSUK_1, CANTOR_1, YELLOW_0, WAYBEL_0, YELLOW_1,
WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL_6,
WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL21, YELLOW13,
WAYBEL29;
constructors TOPS_1, TOPS_2, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL_1, YELLOW_4,
WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29,
COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, TOPS_1,
BORSUK_1, LATTICE3, YELLOW_0, TEX_1, WAYBEL_0, YELLOW_1, YELLOW_2,
YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, YELLOW_6, WAYBEL_8,
WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, YELLOW12, WAYBEL19, YELLOW13,
PRE_TOPC, CARD_1;
requirements BOOLE, SUBSET, NUMERALS;
begin
theorem :: WAYBEL30:1
for x being set, D being non empty set holds x /\ union D = union
the set of all x /\ d where d is Element of D;
theorem :: WAYBEL30:2
for R being non empty reflexive transitive RelStr, D being non
empty directed Subset of InclPoset Ids R holds union D is Ideal of R;
:: Exercise 2.16 (i), p. 16
registration
let R be non empty reflexive transitive RelStr;
cluster InclPoset Ids R -> up-complete;
end;
theorem :: WAYBEL30:3
for R being non empty reflexive transitive RelStr, D being non
empty directed Subset of InclPoset Ids R holds sup D = union D;
theorem :: WAYBEL30:4
for R being Semilattice, D being non empty directed Subset of
InclPoset Ids R, x being Element of InclPoset Ids R holds sup ({x} "/\" D) =
union the set of all x /\ d where d is Element of D;
:: Exercise 4.8 (i), p. 33
registration
let R be Semilattice;
cluster InclPoset Ids R -> satisfying_MC;
end;
registration
let R be 1-element RelStr;
cluster -> trivial for TopAugmentation of R;
end;
theorem :: WAYBEL30:5
for S being Scott complete TopLattice, T being complete LATTICE, A
being Scott TopAugmentation of T st the RelStr of S = the RelStr of T holds the
TopRelStr of A = the TopRelStr of S;
theorem :: WAYBEL30:6
for N being Lawson complete TopLattice, T being complete LATTICE, A
being Lawson correct TopAugmentation of T st the RelStr of N = the RelStr of T
holds the TopRelStr of A = the TopRelStr of N;
theorem :: WAYBEL30:7
for N being Lawson complete TopLattice for S being Scott
TopAugmentation of N for A being Subset of N, J being Subset of S st A = J & J
is closed holds A is closed;
registration
let A be complete LATTICE;
cluster lambda A -> non empty;
end;
registration
let S be Scott complete TopLattice;
cluster InclPoset sigma S -> complete non trivial;
end;
registration
let N be Lawson complete TopLattice;
cluster InclPoset sigma N -> complete non trivial;
cluster InclPoset lambda N -> complete non trivial;
end;
theorem :: WAYBEL30:8
for T being non empty reflexive RelStr holds sigma T c= {W\
uparrow F where W, F is Subset of T: W in sigma T & F is finite};
theorem :: WAYBEL30:9
for N being Lawson complete TopLattice holds lambda N = the topology of N;
theorem :: WAYBEL30:10
for N being Lawson complete TopLattice holds sigma N c= lambda N;
theorem :: WAYBEL30:11
for M, N being complete LATTICE st the RelStr of M = the RelStr of N
holds lambda M = lambda N;
theorem :: WAYBEL30:12
for N being Lawson complete TopLattice, X being Subset of N
holds X in lambda N iff X is open;
registration
cluster TopSpace-like -> Scott for reflexive 1-element TopRelStr;
end;
registration
cluster trivial -> Lawson for complete TopLattice;
end;
registration
cluster strict continuous lower-bounded meet-continuous Scott for complete
TopLattice;
end;
registration
cluster strict continuous compact Hausdorff Lawson for complete TopLattice;
end;
scheme :: WAYBEL30:sch 1
EmptySch { A() -> Scott TopLattice, X() -> set, F(set) -> set }: { F(w)
where w is Element of A(): w in {} } = {};
theorem :: WAYBEL30:13
for N being meet-continuous LATTICE, A being Subset of N st A is
property(S) holds uparrow A is property(S);
registration
let N be meet-continuous LATTICE, A be property(S) Subset of N;
cluster uparrow A -> property(S);
end;
:: Proposition 2.1 (i), p. 153
theorem :: WAYBEL30:14
for N being meet-continuous Lawson complete TopLattice, S
being Scott TopAugmentation of N, A being Subset of N st A in lambda N holds
uparrow A in sigma S;
theorem :: WAYBEL30:15
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for A being Subset of N, J being Subset of S
st A = J holds A is open implies uparrow J is open;
theorem :: WAYBEL30:16
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for x being Point of S, y being Point of N for
J being Basis of y st x = y holds {uparrow A where A is Subset of N: A in J} is
Basis of x;
:: Proposition 2.1 (ii), p. 153
theorem :: WAYBEL30:17
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for X being upper Subset of N, Y being Subset
of S st X = Y holds Int X = Int Y;
:: Proposition 2.1 (iii), p. 153
theorem :: WAYBEL30:18
for N being meet-continuous Lawson complete TopLattice for S being
Scott TopAugmentation of N for X being lower Subset of N, Y being Subset of S
st X = Y holds Cl X = Cl Y;
theorem :: WAYBEL30:19
for M, N being complete LATTICE, LM being Lawson correct
TopAugmentation of M, LN being Lawson correct TopAugmentation of N st InclPoset
sigma N is continuous holds the topology of [:LM,LN qua TopSpace:] = lambda [:M
,N:];
:: Proposition 2.2, p. 153
theorem :: WAYBEL30:20
for M, N being complete LATTICE, P being Lawson correct
TopAugmentation of [:M,N:], Q being Lawson correct TopAugmentation of M, R
being Lawson correct TopAugmentation of N st InclPoset sigma N is continuous
holds the TopStruct of P = [:Q,R qua TopSpace:];
:: Theorem 2.3, p. 153, first conjunct
theorem :: WAYBEL30:21
for N being meet-continuous Lawson complete TopLattice, x
being Element of N holds x"/\" is continuous;
registration
let N be meet-continuous Lawson complete TopLattice, x be Element of N;
cluster x"/\" -> continuous;
end;
:: Theorem 2.3, p. 153, second conjunct
theorem :: WAYBEL30:22
for N being meet-continuous Lawson complete TopLattice st
InclPoset sigma N is continuous holds N is topological_semilattice;
:: Proposition 2.4, p. 153
theorem :: WAYBEL30:23
for N being meet-continuous Lawson complete TopLattice st InclPoset
sigma N is continuous holds N is Hausdorff iff for X being Subset of [:N,N qua
TopSpace:] st X = the InternalRel of N holds X is closed;
:: Definition 2.5, p. 154
definition
let N be non empty reflexive RelStr, X be Subset of N;
func X^0 -> Subset of N equals
:: WAYBEL30:def 1
{ u where u is Element of N : for D being non
empty directed Subset of N st u <= sup D holds X meets D };
end;
registration
let N be non empty reflexive antisymmetric RelStr, X be empty Subset of N;
cluster X^0 -> empty;
end;
theorem :: WAYBEL30:24
for N being non empty reflexive RelStr, A, J being Subset of N st A c=
J holds A^0 c= J^0;
:: Remark 2.6 (i), p. 154
theorem :: WAYBEL30:25
for N being non empty reflexive RelStr, x being Element of N
holds (uparrow x)^0 = wayabove x;
:: Remark 2.6 (ii), p. 154
theorem :: WAYBEL30:26
for N being Scott TopLattice, X being upper Subset of N holds Int X c= X^0;
:: Lemma 2.7 (i), p. 154
theorem :: WAYBEL30:27
for N being non empty reflexive RelStr, X, Y being Subset of N
holds (X^0) \/ (Y^0) c= (X \/ Y)^0;
:: Lemma 2.7 (ii), p. 154
theorem :: WAYBEL30:28
for N being meet-continuous LATTICE, X, Y being upper Subset of
N holds (X^0) \/ (Y^0) = (X \/ Y)^0;
:: Lemma 2.8, p. 154
theorem :: WAYBEL30:29
for S being meet-continuous Scott TopLattice, F being finite
Subset of S holds Int uparrow F c= union { wayabove x where x is Element of S :
x in F };
:: Theorem 2.9, p. 154
theorem :: WAYBEL30:30
for N being Lawson complete TopLattice holds N is continuous
iff N is meet-continuous Hausdorff;
registration
cluster continuous Lawson -> Hausdorff for complete TopLattice;
cluster meet-continuous Lawson Hausdorff -> continuous for
complete TopLattice;
end;
:: Definition 2.10, p. 155
definition
let N be non empty TopRelStr;
attr N is with_small_semilattices means
:: WAYBEL30:def 2
for x being Point of N ex J being
basis of x st for A being Subset of N st A in J holds subrelstr A is
meet-inheriting;
attr N is with_compact_semilattices means
:: WAYBEL30:def 3
for x being Point of N ex J being
basis of x st for A being Subset of N st A in J holds subrelstr A is
meet-inheriting & A is compact;
attr N is with_open_semilattices means
:: WAYBEL30:def 4
for x being Point of N ex J
being Basis of x st for A being Subset of N st A in J holds subrelstr A is
meet-inheriting;
end;
registration
cluster with_open_semilattices -> with_small_semilattices for non empty
TopSpace-like TopRelStr;
cluster with_compact_semilattices -> with_small_semilattices for non empty
TopSpace-like TopRelStr;
cluster anti-discrete -> with_small_semilattices with_open_semilattices for
non
empty TopRelStr;
cluster reflexive TopSpace-like -> with_compact_semilattices
for 1-element TopRelStr;
end;
registration
cluster strict trivial lower for TopLattice;
end;
theorem :: WAYBEL30:31
for N being topological_semilattice with_infima TopPoset, C
being Subset of N st subrelstr C is meet-inheriting holds subrelstr Cl C is
meet-inheriting;
:: Theorem 2.11, p. 155
theorem :: WAYBEL30:32
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N holds (for x being Point of S ex J being Basis
of x st for W being Subset of S st W in J holds W is Filter of S) iff N is
with_open_semilattices;
:: Theorem 2.12, p. 155, r => l
theorem :: WAYBEL30:33
for N being Lawson complete TopLattice for S being Scott
TopAugmentation of N for x being Element of N holds {inf A where A is Subset of
S: x in A & A in sigma S} c= {inf J where J is Subset of N : x in J & J in
lambda N};
:: Theorem 2.12, p. 155
theorem :: WAYBEL30:34
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for x being Element of N holds {inf A where A
is Subset of S : x in A & A in sigma S} = {inf J where J is Subset of N : x in
J & J in lambda N};
:: Theorem 2.13, p. 155, 1 <=> 2
theorem :: WAYBEL30:35
for N being meet-continuous Lawson complete TopLattice holds N
is continuous iff N is with_open_semilattices & InclPoset sigma N is continuous
;
registration
cluster continuous -> with_open_semilattices for
Lawson complete TopLattice;
end;
registration
let N be continuous Lawson complete TopLattice;
cluster InclPoset sigma N -> continuous;
end;
:: Theorem 2.13, p. 155, 1 => 3
theorem :: WAYBEL30:36
for N being continuous Lawson complete TopLattice holds N is compact
Hausdorff topological_semilattice with_open_semilattices;
:: Theorem 2.13, p. 155, 3 => 3'
theorem :: WAYBEL30:37
for N being Hausdorff topological_semilattice with_open_semilattices
Lawson complete TopLattice holds N is with_compact_semilattices;
:: Theorem 2.13, p. 155, 3' => 4
theorem :: WAYBEL30:38
for N being meet-continuous Hausdorff Lawson complete TopLattice, x
being Element of N holds x = "\/"({inf V where V is Subset of N: x in V & V in
lambda N},N);
:: Theorem 2.13, p. 155, 1 <=> 4
theorem :: WAYBEL30:39
for N being meet-continuous Lawson complete TopLattice holds N is
continuous iff for x being Element of N holds x = "\/"({inf V where V is Subset
of N: x in V & V in lambda N},N);
:: Exercise 2.16, p. 156, 1 <=> 2
theorem :: WAYBEL30:40
for N being meet-continuous Lawson complete TopLattice holds N
is algebraic iff N is with_open_semilattices & InclPoset sigma N is algebraic
;
registration
let N be meet-continuous algebraic Lawson complete TopLattice;
cluster InclPoset sigma N -> algebraic;
end;