:: On The Topological Properties of Meet-Continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received December 20, 1996
:: Copyright (c) 1996-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 XBOOLE_0, ORDERS_2, RELAT_1, SEQM_3, FUNCT_1, WAYBEL_0, SUBSET_1,
XXREAL_0, STRUCT_0, SETFAM_1, RELAT_2, LATTICE3, LATTICES, TARSKI,
EQREL_1, WELLORD1, YELLOW_0, CAT_1, ORDINAL2, WAYBEL_2, YELLOW_2,
FINSUB_1, WELLORD2, YELLOW_1, YELLOW_6, PRE_TOPC, RCOMP_1, ZFMISC_1,
ORDERS_1, CARD_1, NATTRA_1, FINSET_1, COMPTS_1, CONNSP_2, ORDINAL1,
TOPS_1, SEQ_2, WAYBEL_7, MCART_1, XXREAL_2, WAYBEL_9;
notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, FINSUB_1,
RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FINSET_1, SETFAM_1, TOLER_1,
PARTFUN1, FUNCT_2, CARD_1, ORDINAL1, NUMBERS, ORDERS_1, DOMAIN_1,
STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, ORDERS_2, COMPTS_1, CONNSP_2,
LATTICE3, ORDERS_3, TDLAT_3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
WAYBEL_1, YELLOW_4, WAYBEL_2, YELLOW_6;
constructors SETFAM_1, DOMAIN_1, FINSUB_1, TOLER_1, TOPS_1, TOPS_2, CONNSP_2,
PCOMPS_1, TDLAT_3, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, YELLOW_6,
COMPTS_1, RELSET_1, XTUPLE_0, XFAMILY;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSUB_1, STRUCT_0,
PRE_TOPC, LATTICE3, YELLOW_0, TDLAT_3, WAYBEL_0, YELLOW_4, WAYBEL_2,
WAYBEL_3, YELLOW_6, COMPTS_1, TOPS_1, CARD_1, XTUPLE_0;
requirements BOOLE, SUBSET;
begin :: Preliminaries
::-------------------------------------------------------------------
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor A. Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------
registration
let L be non empty RelStr;
cluster id L -> monotone;
end;
definition
let S, T be non empty RelStr, f be Function of S,T;
redefine attr f is antitone means
:: WAYBEL_9:def 1
for x, y being Element of S st x <= y holds f.x >= f.y;
end;
theorem :: WAYBEL_9:1
for S, T being RelStr, K, L being non empty RelStr for f being
Function of S, T, g being Function of K, L st the RelStr of S = the RelStr of K
& the RelStr of T = the RelStr of L & f = g & f is monotone holds g is monotone
;
theorem :: WAYBEL_9:2
for S, T being RelStr, K, L being non empty RelStr for f being
Function of S, T, g being Function of K, L st the RelStr of S = the RelStr of K
& the RelStr of T = the RelStr of L & f = g & f is antitone holds g is antitone
;
theorem :: WAYBEL_9:3
for A, B being 1-sorted for F being Subset-Family of A, G being
Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover
of A holds G is Cover of B;
theorem :: WAYBEL_9:4
for L being antisymmetric reflexive with_suprema RelStr, x being
Element of L holds uparrow x = {x} "\/" [#]L;
theorem :: WAYBEL_9:5
for L being antisymmetric reflexive with_infima RelStr, x being
Element of L holds downarrow x = {x} "/\" [#]L;
theorem :: WAYBEL_9:6
for L being antisymmetric reflexive with_infima RelStr, y being
Element of L holds (y"/\").:(uparrow y) = {y};
theorem :: WAYBEL_9:7
for L being antisymmetric reflexive with_infima RelStr, x being
Element of L holds (x"/\")"{x} = uparrow x;
theorem :: WAYBEL_9:8
for T being non empty 1-sorted, N being non empty NetStr over T
holds N is_eventually_in rng the mapping of N;
registration
let L be non empty reflexive RelStr, D be non empty directed Subset of L, n
be Function of D, the carrier of L;
cluster NetStr (#D,(the InternalRel of L)|_2 D,n#) -> directed;
end;
registration
let L be non empty reflexive transitive RelStr, D be non empty directed
Subset of L, n be Function of D, the carrier of L;
cluster NetStr (#D,(the InternalRel of L)|_2 D,n#) -> transitive;
end;
:: cf WAYBEL_2:42
theorem :: WAYBEL_9:9
for L being non empty reflexive transitive RelStr st for x being
Element of L, N being net of L st N is eventually-directed holds x "/\" sup N =
sup ({x} "/\" rng netmap (N,L)) holds L is satisfying_MC;
theorem :: WAYBEL_9:10
for L being non empty RelStr, a being Element of L, N being net
of L holds a "/\" N is net of L;
registration
let L be non empty RelStr, x be Element of L, N be net of L;
cluster x "/\" N -> transitive;
end;
registration
let L be non empty RelStr, x be Element of L, N be non empty reflexive
NetStr over L;
cluster x "/\" N -> reflexive;
end;
registration
let L be non empty RelStr, x be Element of L, N be non empty antisymmetric
NetStr over L;
cluster x "/\" N -> antisymmetric;
end;
registration
let L be non empty RelStr, x be Element of L, N be non empty transitive
NetStr over L;
cluster x "/\" N -> transitive;
end;
registration
let L be non empty RelStr, J be set, f be Function of J,the carrier of L;
cluster FinSups f -> transitive;
end;
begin :: The Operations Defined on Nets
definition
let L be non empty RelStr, N be NetStr over L;
func inf N -> Element of L equals
:: WAYBEL_9:def 2
Inf the mapping of N;
end;
definition
let L be RelStr, N be NetStr over L;
pred ex_sup_of N means
:: WAYBEL_9:def 3
ex_sup_of rng the mapping of N,L;
pred ex_inf_of N means
:: WAYBEL_9:def 4
ex_inf_of rng the mapping of N,L;
end;
definition
let L be RelStr;
func L+id -> strict NetStr over L means
:: WAYBEL_9:def 5
the RelStr of it = the RelStr of L & the mapping of it = id L;
end;
registration
let L be non empty RelStr;
cluster L+id -> non empty;
end;
registration
let L be reflexive RelStr;
cluster L+id -> reflexive;
end;
registration
let L be antisymmetric RelStr;
cluster L+id -> antisymmetric;
end;
registration
let L be transitive RelStr;
cluster L+id -> transitive;
end;
registration
let L be with_suprema RelStr;
cluster L+id -> directed;
end;
registration
let L be directed RelStr;
cluster L+id -> directed;
end;
registration
let L be non empty RelStr;
cluster L+id -> monotone eventually-directed;
end;
definition
let L be RelStr;
func L opp+id -> strict NetStr over L means
:: WAYBEL_9:def 6
the carrier of it = the
carrier of L & the InternalRel of it = (the InternalRel of L)~ & the mapping of
it = id L;
end;
theorem :: WAYBEL_9:11
for L being RelStr holds the RelStr of L~ = the RelStr of L opp+id;
registration
let L be non empty RelStr;
cluster L opp+id -> non empty;
end;
registration
let L be reflexive RelStr;
cluster L opp+id -> reflexive;
end;
registration
let L be antisymmetric RelStr;
cluster L opp+id -> antisymmetric;
end;
registration
let L be transitive RelStr;
cluster L opp+id -> transitive;
end;
registration
let L be with_infima RelStr;
cluster L opp+id -> directed;
end;
registration
let L be non empty RelStr;
cluster L opp+id -> antitone eventually-filtered;
end;
definition
let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;
func N|i -> strict NetStr over L means
:: WAYBEL_9:def 7
(for x being object holds x in
the carrier of it iff ex y being Element of N st y = x & i <= y) & the
InternalRel of it = (the InternalRel of N)|_2 the carrier of it & the mapping
of it = (the mapping of N)|the carrier of it;
end;
theorem :: WAYBEL_9:12
for L being non empty 1-sorted, N being non empty NetStr over L for i
being Element of N holds the carrier of N|i = { y where y is Element of N : i
<= y };
theorem :: WAYBEL_9:13
for L being non empty 1-sorted, N being non empty NetStr over L
for i being Element of N holds the carrier of N|i c= the carrier of N;
theorem :: WAYBEL_9:14
for L being non empty 1-sorted, N being non empty NetStr over L
for i being Element of N holds N|i is full SubNetStr of N;
registration
let L be non empty 1-sorted, N be non empty reflexive NetStr over L, i be
Element of N;
cluster N|i -> non empty reflexive;
end;
registration
let L be non empty 1-sorted, N be non empty directed NetStr over L, i be
Element of N;
cluster N|i -> non empty;
end;
registration
let L be non empty 1-sorted, N be non empty reflexive antisymmetric NetStr
over L, i be Element of N;
cluster N|i -> antisymmetric;
end;
registration
let L be non empty 1-sorted, N be non empty directed antisymmetric NetStr
over L, i be Element of N;
cluster N|i -> antisymmetric;
end;
registration
let L be non empty 1-sorted, N be non empty reflexive transitive NetStr over
L, i be Element of N;
cluster N|i -> transitive;
end;
registration
let L be non empty 1-sorted, N be net of L, i be Element of N;
cluster N|i -> transitive directed;
end;
theorem :: WAYBEL_9:15
for L being non empty 1-sorted, N being non empty reflexive NetStr
over L for i, x being Element of N, x1 being Element of N|i st x = x1 holds N.x
= (N|i).x1;
theorem :: WAYBEL_9:16
for L being non empty 1-sorted, N being non empty directed
NetStr over L for i, x being Element of N, x1 being Element of N|i st x = x1
holds N.x = (N|i).x1;
theorem :: WAYBEL_9:17
for L being non empty 1-sorted, N being net of L, i being
Element of N holds N|i is subnet of N;
registration
let T be non empty 1-sorted, N be net of T;
cluster strict for subnet of N;
end;
definition
let L be non empty 1-sorted, N be net of L, i be Element of N;
redefine func N|i -> strict subnet of N;
end;
definition
let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be
NetStr over S;
func f * N -> strict NetStr over T means
:: WAYBEL_9:def 8
the RelStr of it = the
RelStr of N & the mapping of it = f * the mapping of N;
end;
registration
let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be non
empty NetStr over S;
cluster f * N -> non empty;
end;
registration
let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be
reflexive NetStr over S;
cluster f * N -> reflexive;
end;
registration
let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be
antisymmetric NetStr over S;
cluster f * N -> antisymmetric;
end;
registration
let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be
transitive NetStr over S;
cluster f * N -> transitive;
end;
registration
let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be
directed NetStr over S;
cluster f * N -> directed;
end;
theorem :: WAYBEL_9:18
for L being non empty RelStr, N being non empty NetStr over L
for x being Element of L holds (x"/\")*N = x "/\" N;
begin :: The Properties of Topological Spaces
theorem :: WAYBEL_9:19
for S, T being TopStruct for F being Subset-Family of S, G being
Subset-Family of T st the TopStruct of S = the TopStruct of T & F = G & F is
open holds G is open;
theorem :: WAYBEL_9:20
for S, T being TopStruct for F being Subset-Family of S, G being
Subset-Family of T st the TopStruct of S = the TopStruct of T & F = G & F is
closed holds G is closed;
definition
struct(TopStruct,RelStr) TopRelStr (# carrier -> set, InternalRel -> (
Relation of the carrier), topology -> Subset-Family of the carrier #);
end;
registration
let A be non empty set, R be Relation of A,A, T be Subset-Family of A;
cluster TopRelStr (#A,R,T#) -> non empty;
end;
registration
let x be set, R be Relation of {x};
let T be Subset-Family of {x};
cluster TopRelStr (#{x}, R, T#) -> 1-element;
end;
registration
let X be set, O be Order of X, T be Subset-Family of X;
cluster TopRelStr (#X, O, T#) -> reflexive transitive antisymmetric;
end;
registration
cluster reflexive discrete strict finite 1-element for TopRelStr;
end;
definition
mode TopLattice is with_infima with_suprema reflexive transitive
antisymmetric TopSpace-like TopRelStr;
end;
registration
cluster strict discrete finite compact Hausdorff 1-element for TopLattice;
end;
registration
let T be Hausdorff non empty TopSpace;
cluster -> Hausdorff for non empty SubSpace of T;
end;
theorem :: WAYBEL_9:21
for T being non empty TopSpace, p being Point of T for A being
Element of OpenNeighborhoods p holds A is a_neighborhood of p;
theorem :: WAYBEL_9:22
for T being non empty TopSpace, p being Point of T for A, B
being Element of OpenNeighborhoods p holds A /\ B is Element of
OpenNeighborhoods p;
theorem :: WAYBEL_9:23
for T being non empty TopSpace, p being Point of T for A, B being
Element of OpenNeighborhoods p holds A \/ B is Element of OpenNeighborhoods p
;
theorem :: WAYBEL_9:24
for T being non empty TopSpace, p being Element of T for N being
net of T st p in Lim N for S being Subset of T st S = rng the mapping of N
holds p in Cl S;
theorem :: WAYBEL_9:25
for T being Hausdorff TopLattice, N being convergent net of T
for f being Function of T, T st f is continuous holds f.(lim N) in Lim (f * N);
theorem :: WAYBEL_9:26
for T being Hausdorff TopLattice, N being convergent net of T
for x being Element of T st x"/\" is continuous holds x "/\" lim N in Lim (x
"/\" N);
theorem :: WAYBEL_9:27
for S being Hausdorff TopLattice, x being Element of S st for a
being Element of S holds a"/\" is continuous holds uparrow x is closed;
theorem :: WAYBEL_9:28
for S being compact Hausdorff TopLattice, x being Element of S
st for b being Element of S holds b"/\" is continuous holds downarrow x is
closed;
begin :: The Cluster Points of Nets
definition
let T be non empty TopSpace, N be non empty NetStr over T, p be Point of T;
pred p is_a_cluster_point_of N means
:: WAYBEL_9:def 9
for O being a_neighborhood of p holds N is_often_in O;
end;
theorem :: WAYBEL_9:29
for L being non empty TopSpace, N being net of L for c being Point of
L st c in Lim N holds c is_a_cluster_point_of N;
theorem :: WAYBEL_9:30
for T being compact Hausdorff non empty TopSpace, N being net
of T ex c being Point of T st c is_a_cluster_point_of N;
theorem :: WAYBEL_9:31
for L being non empty TopSpace, N being net of L, M being subnet
of N for c being Point of L st c is_a_cluster_point_of M holds c
is_a_cluster_point_of N;
theorem :: WAYBEL_9:32
for T being non empty TopSpace, N being net of T for x being
Point of T st x is_a_cluster_point_of N holds ex M being subnet of N st x in
Lim M;
theorem :: WAYBEL_9:33
for L being compact Hausdorff non empty TopSpace, N being net
of L st for c, d being Point of L st c is_a_cluster_point_of N & d
is_a_cluster_point_of N holds c = d holds for s being Point of L st s
is_a_cluster_point_of N holds s in Lim N;
theorem :: WAYBEL_9:34
for S being non empty TopSpace, c being Point of S for N being
net of S, A being Subset of S st c is_a_cluster_point_of N & A is closed & rng
the mapping of N c= A holds c in A;
theorem :: WAYBEL_9:35
for S being compact Hausdorff TopLattice, c being Point of S for
N being net of S st (for x being Element of S holds x"/\" is continuous) & N is
eventually-directed & c is_a_cluster_point_of N holds c = sup N;
theorem :: WAYBEL_9:36
for S being compact Hausdorff TopLattice, c being Point of S for
N being net of S st (for x being Element of S holds x"/\" is continuous) & N is
eventually-filtered & c is_a_cluster_point_of N holds c = inf N;
begin :: On The Topological Properties of Meet-Continuous Lattices
:: Proposition 4.4 s. 32 (i) & (ii) => MC
theorem :: WAYBEL_9:37
for S being Hausdorff TopLattice st (for N being net of S st N
is eventually-directed holds ex_sup_of N & sup N in Lim N) & (for x being
Element of S holds x"/\" is continuous) holds S is meet-continuous;
:: Proposition 4.4 s. 32 (ii) => (i)
theorem :: WAYBEL_9:38
for S being compact Hausdorff TopLattice st for x being Element
of S holds x"/\" is continuous holds for N being net of S st N is
eventually-directed holds ex_sup_of N & sup N in Lim N;
:: Proposition 4.4 s. 32 (ii) => (i) dual
theorem :: WAYBEL_9:39
for S being compact Hausdorff TopLattice st for x being Element
of S holds x"/\" is continuous holds for N being net of S st N is
eventually-filtered holds ex_inf_of N & inf N in Lim N;
theorem :: WAYBEL_9:40
for S being compact Hausdorff TopLattice st for x being Element of S
holds x"/\" is continuous holds S is bounded;
theorem :: WAYBEL_9:41
for S being compact Hausdorff TopLattice st for x being Element of S
holds x"/\" is continuous holds S is meet-continuous;