:: On The Topological Properties of Meet-Continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received December 20, 1996
:: Copyright (c) 1996-2026 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;
definitions TARSKI, YELLOW_6, ORDERS_2, WAYBEL_0, WAYBEL_1, YELLOW_0,
PRE_TOPC, WAYBEL_2, LATTICE3, TOPS_2, XBOOLE_0, FINSET_1;
equalities WAYBEL_0, WAYBEL_2, LATTICE3, STRUCT_0, XBOOLE_0, WELLORD1;
expansions TARSKI, YELLOW_6, ORDERS_2, WAYBEL_0, PRE_TOPC, LATTICE3, TOPS_2,
STRUCT_0, XBOOLE_0;
theorems BORSUK_1, COMPTS_1, CONNSP_2, FINSET_1, FUNCT_1, FUNCT_2, ORDERS_2,
ORDERS_1, PCOMPS_1, PRE_TOPC, RELAT_1, SETFAM_1, TARSKI, TOPS_1,
WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4,
YELLOW_6, YELLOW_7, ZFMISC_1, RELSET_1, TDLAT_3, WAYBEL_8, XBOOLE_0,
XBOOLE_1, RELAT_2;
schemes YELLOW_0, FUNCT_2, XBOOLE_0;
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;
coherence by YELLOW_2:11;
end;
definition
let S, T be non empty RelStr, f be Function of S,T;
redefine attr f is antitone means :: redefines antitone (WAYBEL_0, definition)
for x, y being Element of S st x <= y holds f.x >= f.y;
compatibility;
end;
theorem Th1:
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
proof
let S, T be RelStr, K, L be non empty RelStr, f be Function of S, T, g be
Function of K, L such that
A1: the RelStr of S = the RelStr of K and
A2: the RelStr of T = the RelStr of L and
A3: f = g and
A4: f is monotone;
reconsider S1 = S, T1 = T as non empty RelStr by A1,A2;
let x, y be Element of K such that
A5: x <= y;
reconsider x1 = x, y1 = y as Element of S1 by A1;
reconsider f1 = f as Function of S1, T1;
x1 <= y1 by A1,A5;
then f1.x1 <= f1.y1 by A4,WAYBEL_1:def 2;
hence g.x <= g.y by A2,A3;
end;
theorem Th2:
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
proof
let S, T be RelStr, K, L be non empty RelStr, f be Function of S, T, g be
Function of K, L such that
A1: the RelStr of S = the RelStr of K and
A2: the RelStr of T = the RelStr of L and
A3: f = g and
A4: f is antitone;
reconsider S1 = S, T1 = T as non empty RelStr by A1,A2;
let x, y be Element of K such that
A5: x <= y;
reconsider x1 = x, y1 = y as Element of S1 by A1;
reconsider f1 = f as Function of S1, T1;
x1 <= y1 by A1,A5;
then f1.x1 >= f1.y1 by A4;
hence thesis by A2,A3;
end;
theorem
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;
Lm1: for L being antisymmetric reflexive with_infima RelStr, x being Element
of L holds uparrow x = {z where z is Element of L : z "/\" x = x}
proof
let L be antisymmetric reflexive with_infima RelStr, x be Element of L;
thus uparrow x c= {z where z is Element of L : z "/\" x = x}
proof
let q be object;
assume
A1: q in uparrow x;
then reconsider q1 = q as Element of L;
x <= q1 by A1,WAYBEL_0:18;
then q1 "/\" x = x by YELLOW_0:25;
hence thesis;
end;
let q be object;
assume q in {z where z is Element of L : z "/\" x = x};
then consider z being Element of L such that
A2: q = z and
A3: z "/\" x = x;
x <= z by A3,YELLOW_0:25;
hence thesis by A2,WAYBEL_0:18;
end;
theorem Th4:
for L being antisymmetric reflexive with_suprema RelStr, x being
Element of L holds uparrow x = {x} "\/" [#]L
proof
let L be antisymmetric reflexive with_suprema RelStr, x be Element of L;
A1: {x} "\/" [#]L = {x "\/" s where s is Element of L : s in [#] L} by
YELLOW_4:15;
thus uparrow x c= {x} "\/" [#]L
proof
let q be object;
assume
A2: q in uparrow x;
then reconsider q1 = q as Element of L;
x <= q1 by A2,WAYBEL_0:18;
then x "\/" q1 = q1 by YELLOW_0:24;
hence thesis by A1;
end;
let q be object;
assume q in {x} "\/" [#]L;
then consider z being Element of L such that
A3: q = x "\/" z and
z in [#]L by A1;
x <= x "\/" z by YELLOW_0:22;
hence thesis by A3,WAYBEL_0:18;
end;
Lm2: for L being antisymmetric reflexive with_suprema RelStr, x being Element
of L holds downarrow x = {z where z is Element of L : z "\/" x = x}
proof
let L be antisymmetric reflexive with_suprema RelStr, x be Element of L;
thus downarrow x c= {z where z is Element of L : z "\/" x = x}
proof
let q be object;
assume
A1: q in downarrow x;
then reconsider q1 = q as Element of L;
x >= q1 by A1,WAYBEL_0:17;
then q1 "\/" x = x by YELLOW_0:24;
hence thesis;
end;
let q be object;
assume q in {z where z is Element of L : z "\/" x = x};
then consider z being Element of L such that
A2: q = z and
A3: z "\/" x = x;
x >= z by A3,YELLOW_0:24;
hence thesis by A2,WAYBEL_0:17;
end;
theorem Th5:
for L being antisymmetric reflexive with_infima RelStr, x being
Element of L holds downarrow x = {x} "/\" [#]L
proof
let L be antisymmetric reflexive with_infima RelStr, x be Element of L;
A1: {x} "/\" [#]L = {x "/\" s where s is Element of L : s in [#] L} by
YELLOW_4:42;
thus downarrow x c= {x} "/\" [#]L
proof
let q be object;
assume
A2: q in downarrow x;
then reconsider q1 = q as Element of L;
x >= q1 by A2,WAYBEL_0:17;
then x "/\" q1 = q1 by YELLOW_0:25;
hence thesis by A1;
end;
let q be object;
assume q in {x} "/\" [#]L;
then consider z being Element of L such that
A3: q = x "/\" z and
z in [#]L by A1;
x "/\" z <= x by YELLOW_0:23;
hence thesis by A3,WAYBEL_0:17;
end;
theorem
for L being antisymmetric reflexive with_infima RelStr, y being
Element of L holds (y"/\").:(uparrow y) = {y}
proof
let L be antisymmetric reflexive with_infima RelStr, y be Element of L;
thus (y"/\").:(uparrow y) c= {y}
proof
let q be object;
assume q in (y"/\").:(uparrow y);
then consider a being object such that
a in dom (y"/\") and
A1: a in uparrow y and
A2: q = (y"/\").a by FUNCT_1:def 6;
reconsider a as Element of L by A1;
A3: y <= a by A1,WAYBEL_0:18;
q = y "/\" a by A2,WAYBEL_1:def 18
.= y by A3,YELLOW_0:25;
hence thesis by TARSKI:def 1;
end;
let q be object;
assume q in {y};
then
A4: q = y by TARSKI:def 1;
y <= y;
then
A5: dom (y"/\") = the carrier of L & y in uparrow y by FUNCT_2:def 1
,WAYBEL_0:18;
y = y "/\" y by YELLOW_0:25
.= (y"/\").y by WAYBEL_1:def 18;
hence thesis by A4,A5,FUNCT_1:def 6;
end;
theorem Th7:
for L being antisymmetric reflexive with_infima RelStr, x being
Element of L holds (x"/\")"{x} = uparrow x
proof
let L be antisymmetric reflexive with_infima RelStr, x be Element of L;
thus (x"/\")"{x} c= uparrow x
proof
let q be object;
assume
A1: q in (x"/\")"{x};
then reconsider q1 = q as Element of L;
A2: (x"/\").q1 in {x} by A1,FUNCT_1:def 7;
x "/\" q1 = (x"/\").q1 by WAYBEL_1:def 18
.= x by A2,TARSKI:def 1;
then x <= q1 by YELLOW_0:25;
hence thesis by WAYBEL_0:18;
end;
let q be object;
assume
A3: q in uparrow x;
then reconsider q1 = q as Element of L;
A4: x <= q1 by A3,WAYBEL_0:18;
(x"/\").q1 = x "/\" q1 by WAYBEL_1:def 18
.= x by A4,YELLOW_0:25;
then dom (x"/\") = the carrier of L & (x"/\").q1 in {x} by FUNCT_2:def 1
,TARSKI:def 1;
hence thesis by FUNCT_1:def 7;
end;
theorem Th8:
for T being non empty 1-sorted, N being non empty NetStr over T
holds N is_eventually_in rng the mapping of N
proof
let T be non empty 1-sorted, N be non empty NetStr over T;
set i = the Element of N;
take i;
let j be Element of N such that
i <= j;
thus thesis by FUNCT_2:4;
end;
:: cf WAYBEL_2:19
Lm3: for L being non empty reflexive transitive RelStr for D being non empty
directed Subset of L for n being Function of D, the carrier of L holds NetStr
(#D,(the InternalRel of L)|_2 D,n#) is net of L
proof
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;
set N = NetStr (#D,(the InternalRel of L)|_2 D,n#);
the InternalRel of N c= the InternalRel of L by XBOOLE_1:17;
then reconsider N as SubRelStr of L by YELLOW_0:def 13;
reconsider N as full SubRelStr of L by YELLOW_0:def 14;
N is directed
proof
let x, y be Element of N;
assume that
x in [#]N and
y in [#]N;
reconsider x1 = x, y1 = y as Element of D;
consider z1 being Element of L such that
A1: z1 in D and
A2: x1 <= z1 & y1 <= z1 by WAYBEL_0:def 1;
reconsider z = z1 as Element of N by A1;
take z;
thus z in [#]N;
thus thesis by A2,YELLOW_0:60;
end;
then reconsider N as prenet of L;
N is transitive;
hence thesis;
end;
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;
coherence by WAYBEL_2:19;
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;
coherence by Lm3;
end;
:: cf WAYBEL_2:42
theorem Th9:
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
proof
let L be non empty reflexive transitive RelStr such that
A1: 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));
let x be Element of L, D be non empty directed Subset of L;
reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7;
set N = NetStr (#D,(the InternalRel of L)|_2 D,n#);
A2: N is eventually-directed & Sup netmap (N,L) = sup N by WAYBEL_2:20;
D c= D;
then
A3: D = n.:D by FUNCT_1:92
.= rng netmap (N,L) by RELSET_1:22;
hence x "/\" sup D = x "/\" Sup netmap (N,L) by YELLOW_2:def 5
.= sup ({x} "/\" D) by A1,A3,A2;
end;
theorem Th10:
for L being non empty RelStr, a being Element of L, N being net
of L holds a "/\" N is net of L
proof
let L be non empty RelStr, a be Element of L, N be net of L;
set aN = a "/\" N;
aN is transitive
proof
let x, y, z be Element of aN such that
A1: x <= y & y <= z;
reconsider x1 = x, y1 = y, z1 = z as Element of N by WAYBEL_2:22;
A2: the RelStr of N = the RelStr of aN by WAYBEL_2:def 3;
then x1 <= y1 & y1 <= z1 by A1;
then x1 <= z1 by YELLOW_0:def 2;
hence thesis by A2;
end;
hence thesis;
end;
registration
let L be non empty RelStr, x be Element of L, N be net of L;
cluster x "/\" N -> transitive;
coherence by Th10;
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;
coherence
proof
the RelStr of N = the RelStr of x "/\" N by WAYBEL_2:def 3;
then
the InternalRel of x "/\" N is_reflexive_in the carrier of x "/\" N by
ORDERS_2:def 2;
hence thesis;
end;
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;
coherence
proof
the RelStr of N = the RelStr of x "/\" N by WAYBEL_2:def 3;
then
the InternalRel of x "/\" N is_antisymmetric_in the carrier of x "/\"
N by ORDERS_2:def 4;
hence thesis;
end;
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;
coherence
proof
the RelStr of N = the RelStr of x "/\" N by WAYBEL_2:def 3;
then the InternalRel of x "/\" N is_transitive_in the carrier of x "/\" N
by ORDERS_2:def 3;
hence thesis;
end;
end;
registration
let L be non empty RelStr, J be set, f be Function of J,the carrier of L;
cluster FinSups f -> transitive;
coherence
proof
let x, y, z be Element of FinSups f such that
A1: x <= y and
A2: y <= z;
A3: (ex g being Function of Fin J, the carrier of L st for x being Element
of Fin J holds g.x = sup (f.:x) & FinSups f = NetStr (# Fin J, RelIncl Fin J, g
#) )& InclPoset Fin J = RelStr(#Fin J, RelIncl Fin J#) by WAYBEL_2:def 2
,YELLOW_1:def 1;
then reconsider x1 = x, y1 = y, z1 = z as Element of InclPoset Fin J;
y1 <= z1 by A2,A3;
then
A4: y1 c= z1 by YELLOW_1:3;
x1 <= y1 by A1,A3;
then x1 c= y1 by YELLOW_1:3;
then x1 c= z1 by A4;
then x1 <= z1 by YELLOW_1:3;
hence thesis by A3;
end;
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
Inf the mapping of N;
coherence;
end;
definition
let L be RelStr, N be NetStr over L;
pred ex_sup_of N means
ex_sup_of rng the mapping of N,L;
pred ex_inf_of N means
ex_inf_of rng the mapping of N,L;
end;
definition
let L be RelStr;
func L+id -> strict NetStr over L means
:Def5:
the RelStr of it = the RelStr of L & the mapping of it = id L;
existence
proof
take NetStr (#the carrier of L, the InternalRel of L, id L#);
thus thesis;
end;
uniqueness;
end;
registration
let L be non empty RelStr;
cluster L+id -> non empty;
coherence
proof
the RelStr of L = the RelStr of L+id by Def5;
hence thesis;
end;
end;
registration
let L be reflexive RelStr;
cluster L+id -> reflexive;
coherence
proof
the RelStr of L = the RelStr of L+id by Def5;
then the InternalRel of L+id is_reflexive_in the carrier of L+id by
ORDERS_2:def 2;
hence thesis;
end;
end;
registration
let L be antisymmetric RelStr;
cluster L+id -> antisymmetric;
coherence
proof
the RelStr of L = the RelStr of L+id by Def5;
then the InternalRel of L+id is_antisymmetric_in the carrier of L+id by
ORDERS_2:def 4;
hence thesis;
end;
end;
registration
let L be transitive RelStr;
cluster L+id -> transitive;
coherence
proof
the RelStr of L = the RelStr of L+id by Def5;
then the InternalRel of L+id is_transitive_in the carrier of L+id by
ORDERS_2:def 3;
hence thesis;
end;
end;
registration
let L be with_suprema RelStr;
cluster L+id -> directed;
coherence
proof
A1: the RelStr of L = the RelStr of L+id by Def5;
then [#]L = [#](L+id);
hence [#](L+id) is directed by A1,WAYBEL_0:3;
end;
end;
registration
let L be directed RelStr;
cluster L+id -> directed;
coherence
proof
[#]L is directed & the RelStr of L = the RelStr of L+id by Def5,
WAYBEL_0:def 6;
hence [#](L+id) is directed by WAYBEL_0:3;
end;
end;
registration
let L be non empty RelStr;
cluster L+id -> monotone eventually-directed;
coherence
proof
set N = L+id;
netmap(N,L) = id L & the RelStr of N = the RelStr of L by Def5;
then netmap(L+id,L) is monotone by Th1;
hence N is monotone;
for i being Element of N ex j being Element of N st for k being
Element of N st j <= k holds N.i <= N.k
proof
let i be Element of N;
take j = i;
let k be Element of N such that
A1: j <= k;
A2: the RelStr of N = the RelStr of L by Def5;
the mapping of N = id L by Def5;
then (the mapping of N).i = i & (the mapping of N).k = k by A2;
hence thesis by A1,A2;
end;
hence thesis by WAYBEL_0:11;
end;
end;
definition
let L be RelStr;
func L opp+id -> strict NetStr over L means
:Def6:
the carrier of it = the
carrier of L & the InternalRel of it = (the InternalRel of L)~ & the mapping of
it = id L;
existence
proof
take NetStr (#the carrier of L, (the InternalRel of L)~, id L#);
thus thesis;
end;
uniqueness;
end;
theorem Th11:
for L being RelStr holds the RelStr of L~ = the RelStr of L opp+id
proof
let L be RelStr;
the InternalRel of L~ = the InternalRel of L opp+id by Def6;
hence thesis by Def6;
end;
registration
let L be non empty RelStr;
cluster L opp+id -> non empty;
coherence
proof
the RelStr of L~ = the RelStr of L opp+id by Th11;
hence thesis;
end;
end;
registration
let L be reflexive RelStr;
cluster L opp+id -> reflexive;
coherence
proof
the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;
then
A1: (the InternalRel of L)~ is_reflexive_in the carrier of L by ORDERS_1:79;
the InternalRel of L opp+id = (the InternalRel of L)~ by Def6;
hence the InternalRel of L opp+id is_reflexive_in the carrier of L opp+id
by A1,Def6;
end;
end;
registration
let L be antisymmetric RelStr;
cluster L opp+id -> antisymmetric;
coherence
proof
the InternalRel of L is_antisymmetric_in the carrier of L by ORDERS_2:def 4
;
then
A1: (the InternalRel of L)~ is_antisymmetric_in the carrier of L by ORDERS_1:81
;
the InternalRel of L opp+id = (the InternalRel of L)~ by Def6;
then the InternalRel of L opp+id is_antisymmetric_in the carrier of L
opp+id by A1,Def6;
hence thesis;
end;
end;
registration
let L be transitive RelStr;
cluster L opp+id -> transitive;
coherence
proof
the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def 3;
then
A1: (the InternalRel of L)~ is_transitive_in the carrier of L by ORDERS_1:80;
the InternalRel of L opp+id = (the InternalRel of L)~ by Def6;
then the InternalRel of L opp+id is_transitive_in the carrier of L opp+id
by A1,Def6;
hence thesis;
end;
end;
registration
let L be with_infima RelStr;
cluster L opp+id -> directed;
coherence
proof
reconsider A = L~ as with_suprema RelStr by YELLOW_7:16;
the RelStr of L~ = the RelStr of L opp+id & [#]A = [#](L opp+id) by Def6
,Th11;
hence [#](L opp+id) is directed by WAYBEL_0:3;
end;
end;
registration
let L be non empty RelStr;
cluster L opp+id -> antitone eventually-filtered;
coherence
proof
set N = L opp+id;
thus N is antitone
proof
reconsider f = id L as Function of L~, L;
reconsider g = f as Function of L, L~;
g is antitone by YELLOW_7:40;
then
A1: the RelStr of L = the RelStr of L & f is antitone by YELLOW_7:41;
netmap(N,L) = id L & the RelStr of L opp+id = the RelStr of L~ by Def6
,Th11;
hence netmap(N,L) is antitone by A1,Th2;
end;
for i being Element of N ex j being Element of N st for k being
Element of N st j <= k holds N.i >= N.k
proof
let i be Element of N;
take j = i;
A2: the mapping of N = id L & the InternalRel of N = (the InternalRel of
L)~ by Def6;
let k be Element of N;
assume j <= k;
then [i,k] in the InternalRel of N;
then
A3: [k,i] in (the InternalRel of N)~ by RELAT_1:def 7;
reconsider i1 = i, k1 = k as Element of L by Def6;
(id L).i1 = i1 & (id L).k1 = k1;
hence thesis by A2,A3;
end;
hence thesis by WAYBEL_0:12;
end;
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
:Def7:
(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;
existence
proof
defpred P[object] means ex y being Element of N st y = $1 & i <= y;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of N & P[x] from
XBOOLE_0:sch 1;
X c= the carrier of N
by A1;
then reconsider
f = (the mapping of N)|X as Function of X, the carrier of L by FUNCT_2:32;
set IT = NetStr (#X, (the InternalRel of N)|_2 X, f#);
take IT;
thus for x being object
holds x in the carrier of IT iff ex y being Element
of N st y = x & i <= y by A1;
thus thesis;
end;
uniqueness
proof
defpred P[object] means ex y being Element of N st y = $1 & i <= y;
let A, B be strict NetStr over L such that
A2: for x being object holds x in the carrier of A iff P[x] and
A3: the InternalRel of A = (the InternalRel of N)|_2 the carrier of A
& the mapping of A = (the mapping of N)|the carrier of A and
A4: for x being object holds x in the carrier of B iff P[x] and
A5: the InternalRel of B = (the InternalRel of N)|_2 the carrier of B
& the mapping of B = (the mapping of N)|the carrier of B;
the carrier of A = the carrier of B from XBOOLE_0:sch 2(A2, A4);
hence thesis by A3,A5;
end;
end;
theorem
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 }
proof
let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;
thus the carrier of N|i c= { y where y is Element of N : i <= y }
proof
let q be object;
assume q in the carrier of N|i;
then ex y being Element of N st y = q & i <= y by Def7;
hence thesis;
end;
let q be object;
assume q in { y where y is Element of N : i <= y };
then ex y being Element of N st q = y & i <= y;
hence thesis by Def7;
end;
theorem Th13:
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
proof
let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;
let x be object;
assume x in the carrier of N|i;
then ex y being Element of N st y = x & i <= y by Def7;
hence thesis;
end;
theorem Th14:
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
proof
let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;
A1: the mapping of N|i = (the mapping of N)|the carrier of N|i by Def7;
the InternalRel of N|i = (the InternalRel of N)|_2 the carrier of N|i by Def7
;
then
A2: the InternalRel of N|i c= the InternalRel of N by XBOOLE_1:17;
the carrier of N|i c= the carrier of N by Th13;
then N|i is SubRelStr of N by A2,YELLOW_0:def 13;
then reconsider K = N|i as SubNetStr of N by A1,YELLOW_6:def 6;
the InternalRel of K = (the InternalRel of N)|_2 the carrier of K by Def7;
then K is full SubRelStr of N by YELLOW_0:def 14,YELLOW_6:def 6;
hence thesis by YELLOW_6:def 7;
end;
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;
coherence
proof
A1: i <= i;
hence N|i is non empty by Def7;
reconsider A = N|i as strict non empty NetStr over L by A1,Def7;
A is reflexive
proof
let x be Element of A;
consider y being Element of N such that
A2: y = x and
i <= y by Def7;
N|i is full SubNetStr of N & y <= y by Th14;
hence thesis by A2,YELLOW_6:12;
end;
hence thesis;
end;
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;
coherence
proof
ex z1 being Element of N st i <= z1 & i <= z1 by YELLOW_6:def 3;
hence thesis by Def7;
end;
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;
coherence
proof
let x, y be Element of N|i such that
A1: x <= y & y <= x;
consider y1 being Element of N such that
A2: y1 = y and
i <= y1 by Def7;
consider x1 being Element of N such that
A3: x1 = x and
i <= x1 by Def7;
N|i is SubNetStr of N by Th14;
then x1 <= y1 & y1 <= x1 by A1,A3,A2,YELLOW_6:11;
hence thesis by A3,A2,YELLOW_0:def 3;
end;
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;
coherence
proof
let x, y be Element of N|i such that
A1: x <= y & y <= x;
consider y1 being Element of N such that
A2: y1 = y and
i <= y1 by Def7;
consider x1 being Element of N such that
A3: x1 = x and
i <= x1 by Def7;
N|i is SubNetStr of N by Th14;
then x1 <= y1 & y1 <= x1 by A1,A3,A2,YELLOW_6:11;
hence thesis by A3,A2,YELLOW_0:def 3;
end;
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;
coherence
proof
let x, y, z be Element of N|i such that
A1: x <= y and
A2: y <= z;
consider z1 being Element of N such that
A3: z1 = z and
i <= z1 by Def7;
consider x1 being Element of N such that
A4: x1 = x and
i <= x1 by Def7;
consider y1 being Element of N such that
A5: y1 = y and
i <= y1 by Def7;
A6: N|i is full SubNetStr of N by Th14;
then
A7: y1 <= z1 by A2,A5,A3,YELLOW_6:11;
x1 <= y1 by A1,A6,A4,A5,YELLOW_6:11;
then x1 <= z1 by A7,YELLOW_0:def 2;
hence x <= z by A6,A4,A3,YELLOW_6:12;
end;
end;
registration
let L be non empty 1-sorted, N be net of L, i be Element of N;
cluster N|i -> transitive directed;
coherence
proof
thus N|i is transitive
proof
let x, y, z be Element of N|i such that
A1: x <= y and
A2: y <= z;
consider z1 being Element of N such that
A3: z1 = z and
i <= z1 by Def7;
consider x1 being Element of N such that
A4: x1 = x and
i <= x1 by Def7;
consider y1 being Element of N such that
A5: y1 = y and
i <= y1 by Def7;
A6: N|i is full SubNetStr of N by Th14;
then
A7: y1 <= z1 by A2,A5,A3,YELLOW_6:11;
x1 <= y1 by A1,A6,A4,A5,YELLOW_6:11;
then x1 <= z1 by A7,YELLOW_0:def 2;
hence thesis by A6,A4,A3,YELLOW_6:12;
end;
for x, y being Element of N|i ex z being Element of N|i st x <= z & y <= z
proof
let x, y be Element of N|i;
consider x1 being Element of N such that
A8: x1 = x and
A9: i <= x1 by Def7;
consider y1 being Element of N such that
A10: y1 = y and
i <= y1 by Def7;
consider z1 being Element of N such that
A11: x1 <= z1 and
A12: y1 <= z1 by YELLOW_6:def 3;
i <= z1 by A9,A11,YELLOW_0:def 2;
then reconsider z = z1 as Element of N|i by Def7;
take z;
N|i is full SubNetStr of N by Th14;
hence thesis by A8,A10,A11,A12,YELLOW_6:12;
end;
hence thesis;
end;
end;
theorem
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
proof
let L be non empty 1-sorted, N be non empty reflexive NetStr over L, i, x be
Element of N, x1 be Element of N|i;
assume x = x1;
hence N.x = ((the mapping of N)|(the carrier of N|i)).x1 by FUNCT_1:49
.= (N|i).x1 by Def7;
end;
theorem Th16:
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
proof
let L be non empty 1-sorted, N be non empty directed NetStr over L, i, x be
Element of N, x1 be Element of N|i;
assume x = x1;
hence N.x = ((the mapping of N)|(the carrier of N|i)).x1 by FUNCT_1:49
.= (N|i).x1 by Def7;
end;
theorem Th17:
for L being non empty 1-sorted, N being net of L, i being
Element of N holds N|i is subnet of N
proof
let L be non empty 1-sorted, N be net of L, i be Element of N;
reconsider A = N|i as net of L;
A1: the carrier of A c= the carrier of N by Th13;
A is subnet of N
proof
reconsider f = id the carrier of A as Function of A, N by A1,FUNCT_2:7;
take f;
for x being object st x in the carrier of A holds (the mapping of A).x =
((the mapping of N)*f).x
proof
let x be object such that
A2: x in the carrier of A;
thus (the mapping of A).x = ((the mapping of N)|the carrier of A).x by
Def7
.= (the mapping of N).x by A2,FUNCT_1:49
.= (the mapping of N).(f.x) by A2,FUNCT_1:18
.= ((the mapping of N)*f).x by A2,FUNCT_2:15;
end;
hence the mapping of A = (the mapping of N)*f by FUNCT_2:12;
let m be Element of N;
consider z being Element of N such that
A3: i <= z and
A4: m <= z by YELLOW_6:def 3;
reconsider n = z as Element of A by A3,Def7;
take n;
let p be Element of A such that
A5: n <= p;
reconsider p1 = p as Element of N by A1;
A is SubNetStr of N by Th14;
then z <= p1 by A5,YELLOW_6:11;
then m <= p1 by A4,YELLOW_0:def 2;
hence thesis;
end;
hence thesis;
end;
registration
let T be non empty 1-sorted, N be net of T;
cluster strict for subnet of N;
existence
proof
set A = NetStr (#the carrier of N,the InternalRel of N,the mapping of N#);
A1: the RelStr of A = the RelStr of N;
[#]N is directed by WAYBEL_0:def 6;
then [#]A is directed by A1,WAYBEL_0:3;
then reconsider A as net of T by A1,WAYBEL_0:def 6,WAYBEL_8:13;
A is subnet of N
proof
reconsider f = id N as Function of A, N;
take f;
thus the mapping of A = (the mapping of N)*f by FUNCT_2:17;
let m be Element of N;
reconsider n = m as Element of A;
take n;
let p be Element of A such that
A2: n <= p;
thus thesis by A2;
end;
then reconsider A as subnet of N;
take A;
thus thesis;
end;
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; :: redefines | (WAYBEL_9, definition)
coherence by Th17;
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
:Def8:
the RelStr of it = the
RelStr of N & the mapping of it = f * the mapping of N;
existence
proof
take NetStr (#the carrier of N, the InternalRel of N, f*the mapping of N#);
thus thesis;
end;
uniqueness;
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;
coherence
proof
the RelStr of N = the RelStr of f * N by Def8;
hence thesis;
end;
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;
coherence
proof
the RelStr of N = the RelStr of f * N by Def8;
hence the InternalRel of f*N is_reflexive_in the carrier of f*N by
ORDERS_2:def 2;
end;
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;
coherence
proof
the RelStr of N = the RelStr of f * N by Def8;
then the InternalRel of f*N is_antisymmetric_in the carrier of f*N by
ORDERS_2:def 4;
hence thesis;
end;
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;
coherence
proof
the RelStr of N = the RelStr of f * N by Def8;
then the InternalRel of f*N is_transitive_in the carrier of f*N by
ORDERS_2:def 3;
hence thesis;
end;
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;
coherence
proof
the RelStr of N = the RelStr of f * N & [#]N is directed by Def8,
WAYBEL_0:def 6;
hence [#](f*N) is directed by WAYBEL_0:3;
end;
end;
theorem Th18:
for L being non empty RelStr, N being non empty NetStr over L
for x being Element of L holds (x"/\")*N = x "/\" N
proof
let L be non empty RelStr, N be non empty NetStr over L, x be Element of L;
set n = the mapping of N;
A1: the RelStr of (x"/\")*N = the RelStr of N by Def8
.= the RelStr of x "/\" N by WAYBEL_2:def 3;
A2: the RelStr of N = the RelStr of x "/\" N by WAYBEL_2:def 3;
then reconsider
f2 = the mapping of x "/\" N as Function of the carrier of N, the
carrier of L;
A3: for c being Element of N holds ((x"/\") * n).c = f2.c
proof
let c be Element of N;
consider y being Element of L such that
A4: y = n.c and
A5: f2.c = x "/\" y by A2,WAYBEL_2:def 3;
thus ((x"/\") * n).c = (x"/\").y by A4,FUNCT_2:15
.= f2.c by A5,WAYBEL_1:def 18;
end;
the mapping of (x"/\")*N = (x"/\") * n by Def8
.= the mapping of x "/\" N by A3,FUNCT_2:63;
hence thesis by A1;
end;
begin :: The Properties of Topological Spaces
theorem
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
proof
let S, T be TopStruct, F be Subset-Family of S, G be Subset-Family of T such
that
A1: the TopStruct of S = the TopStruct of T and
A2: F = G & F is open;
let P be Subset of T such that
A3: P in G;
reconsider R = P as Subset of S by A1;
R is open by A2,A3;
hence P in the topology of T by A1;
end;
theorem
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
proof
let S, T be TopStruct, F be Subset-Family of S, G be Subset-Family of T such
that
A1: the TopStruct of S = the TopStruct of T and
A2: F = G & F is closed;
let P be Subset of T such that
A3: P in G;
reconsider R = P as Subset of S by A1;
R is closed by A2,A3;
then [#]S \ R is open;
hence [#]T \ P in the topology of T by A1;
end;
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;
coherence;
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;
coherence;
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;
coherence
proof
set A = TopRelStr(#X,O,T#);
A1: field the InternalRel of A = the carrier of A by ORDERS_1:12;
then
A2: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 12
;
the InternalRel of A is_reflexive_in the carrier of A & the
InternalRel of A is_transitive_in the carrier of A by A1,RELAT_2:def 9,def 16;
hence thesis by A2;
end;
end;
Lm4: for tau being Subset-Family of {0}, r being Relation of {0} st tau = {{},
{0}} & r = {[0,0]} holds TopRelStr (#{0},r,tau#)
is reflexive discrete finite 1-element
proof
let tau be Subset-Family of {0}, r be Relation of {0} such that
A1: tau = {{},{0}} and
A2: r = {[0,0]};
set T = TopRelStr (#{0},r,tau#);
thus T is reflexive
proof
let x be Element of T;
x = 0 by TARSKI:def 1;
then [x,x] in {[0,0]} by TARSKI:def 1;
hence thesis by A2;
end;
the topology of T = bool the carrier of T by A1,ZFMISC_1:24;
hence T is discrete by TDLAT_3:def 1;
thus thesis;
end;
registration
cluster reflexive discrete strict finite 1-element for TopRelStr;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
{{},{0}} = bool {0} by ZFMISC_1:24;
then reconsider tau = {{},{0}} as Subset-Family of {0};
take TopRelStr (#{0},r,tau#);
thus thesis by Lm4;
end;
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;
existence
proof
reconsider C = bool {0} as Subset-Family of {0};
0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
{{},{0}} = bool {0} by ZFMISC_1:24;
then reconsider A = TopRelStr (#{0}, r, C#)
as reflexive discrete finite 1-element TopRelStr by Lm4;
reconsider A as TopLattice;
take A;
thus A is strict discrete finite;
thus A is compact;
thus A is Hausdorff
proof let p, q be Point of A such that
A1: not p = q;
p = 0 by TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
thus thesis;
end;
end;
registration
let T be Hausdorff non empty TopSpace;
cluster -> Hausdorff for non empty SubSpace of T;
coherence;
end;
theorem Th21:
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
proof
let T be non empty TopSpace, p be Point of T, A be Element of
OpenNeighborhoods p;
ex W being Subset of T st W = A & p in W & W is open by YELLOW_6:29;
hence thesis by CONNSP_2:3;
end;
theorem Th22:
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
proof
let T be non empty TopSpace, p be Point of T, A, B be Element of
OpenNeighborhoods p;
consider W being Subset of T such that
A1: W = A and
A2: p in W & W is open by YELLOW_6:29;
consider X being Subset of T such that
A3: X = B and
A4: p in X & X is open by YELLOW_6:29;
p in A /\ B & W /\ X is open by A1,A2,A3,A4,XBOOLE_0:def 4;
hence thesis by A1,A3,YELLOW_6:30;
end;
theorem
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
proof
let T be non empty TopSpace, p be Point of T, A, B be Element of
OpenNeighborhoods p;
consider W being Subset of T such that
A1: W = A and
A2: p in W and
A3: W is open by YELLOW_6:29;
A4: p in A \/ B by A1,A2,XBOOLE_0:def 3;
consider X being Subset of T such that
A5: X = B and
p in X and
A6: X is open by YELLOW_6:29;
W \/ X is open by A3,A6;
hence thesis by A1,A5,A4,YELLOW_6:30;
end;
theorem Th24:
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
proof
let T be non empty TopSpace, p be Element of T, N be net of T such that
A1: p in Lim N;
let S be Subset of T;
assume S = rng the mapping of N;
then
A2: N is_eventually_in S by Th8;
for G being Subset of T st G is open holds p in G implies S meets G
proof
let G be Subset of T such that
A3: G is open and
A4: p in G;
G = Int G by A3,TOPS_1:23;
then reconsider V = G as a_neighborhood of p by A4,CONNSP_2:def 1;
N is_eventually_in V by A1,YELLOW_6:def 15;
hence thesis by A2,YELLOW_6:17;
end;
hence thesis by PRE_TOPC:def 7;
end;
theorem Th25:
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)
proof
let T be Hausdorff TopLattice, N be convergent net of T, f be Function of T,
T such that
A1: f is continuous;
for V being a_neighborhood of f.(lim N) holds f*N is_eventually_in V
proof
let V be a_neighborhood of f.(lim N);
A2: dom f = the carrier of T by FUNCT_2:def 1;
consider O being a_neighborhood of lim N such that
A3: f.:O c= V by A1,BORSUK_1:def 1;
lim N in Lim N by YELLOW_6:def 17;
then N is_eventually_in O by YELLOW_6:def 15;
then consider s0 being Element of N such that
A4: for j being Element of N st s0 <= j holds N.j in O;
A5: the RelStr of f*N = the RelStr of N by Def8;
then reconsider s1 = s0 as Element of f*N;
take s1;
let j1 be Element of f*N such that
A6: s1 <= j1;
reconsider j = j1 as Element of N by A5;
N.j in O by A4,A5,A6,YELLOW_0:1;
then
A7: f.(N.j) in f.:O by A2,FUNCT_1:def 6;
A8: the carrier of f*N = dom the mapping of N by A5,FUNCT_2:def 1;
(f*N).j1 = (f * the mapping of N).j1 by Def8
.= f.(N.j) by A8,FUNCT_1:13;
hence thesis by A3,A7;
end;
hence thesis by YELLOW_6:def 15;
end;
theorem Th26:
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)
proof
let T be Hausdorff TopLattice, N be convergent net of T, x be Element of T
such that
A1: x"/\" is continuous;
x "/\" lim N = (x"/\").(lim N) by WAYBEL_1:def 18;
then x "/\" lim N in Lim (x"/\" * N) by A1,Th25;
hence thesis by Th18;
end;
theorem Th27:
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
proof
let S be Hausdorff TopLattice, x be Element of S;
assume for a being Element of S holds a"/\" is continuous;
then
A1: x"/\" is continuous;
(x"/\")"{x} = uparrow x & {x} is closed by Th7,PCOMPS_1:7;
hence thesis by A1;
end;
theorem Th28:
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
proof
let S be compact Hausdorff TopLattice, b be Element of S;
assume for a being Element of S holds a"/\" is continuous;
then
A1: b"/\" is continuous;
set g1 = (rng (b"/\"))|`(b"/\");
A2: g1 = b"/\" by RELAT_1:94;
A3: dom (b"/\") = the carrier of S by FUNCT_2:def 1;
A4: {b} "/\" [#]S = {b "/\" y where y is Element of S: y in [#] S} by
YELLOW_4:42;
A5: rng (b"/\") = {b} "/\" [#]S
proof
thus rng (b"/\") c= {b} "/\" [#]S
proof
let q be object;
assume q in rng (b"/\");
then consider x being object such that
A6: x in dom (b"/\") and
A7: (b"/\").x = q by FUNCT_1:def 3;
reconsider x1 = x as Element of S by A6;
q = b "/\" x1 by A7,WAYBEL_1:def 18;
hence thesis by A4;
end;
let q be object;
assume q in {b} "/\" [#]S;
then consider y being Element of S such that
A8: q = b "/\" y and
y in [#]S by A4;
q = (b"/\").y by A8,WAYBEL_1:def 18;
hence thesis by A3,FUNCT_1:def 3;
end;
then rng g1 = {b} "/\" [#]S by RELAT_1:94
.= [#](S | (rng (b"/\"))) by A5,PRE_TOPC:def 5
.= the carrier of S|(rng(b"/\"));
then reconsider g1 as Function of S, S|(rng (b"/\")) by A2,A3,FUNCT_2:1;
rng g1 = {b} "/\" [#]S by A5,RELAT_1:94
.= [#](S | ({b}"/\"[#]S)) by PRE_TOPC:def 5;
then S | ({b} "/\" [#]S) is compact by A1,A2,A5,COMPTS_1:14,PRE_TOPC:27;
then {b} "/\" [#]S is compact by COMPTS_1:3;
hence thesis by Th5;
end;
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
for O being a_neighborhood of p holds N is_often_in O;
end;
theorem
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
proof
let L be non empty TopSpace, N be net of L, c be Point of L such that
A1: c in Lim N;
let O be a_neighborhood of c;
N is_eventually_in O by A1,YELLOW_6:def 15;
hence thesis by YELLOW_6:19;
end;
theorem Th30:
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
proof
let T be compact Hausdorff non empty TopSpace, N be net of T;
defpred P[set,set] means ex X being Subset of T, a being Element of N st a =
$1 & X = {N.j where j is Element of N : a <= j} & $2 = Cl X;
A1: for e being Element of N ex u being Subset of T st P[e,u]
proof
let e be Element of N;
reconsider a = e as Element of N;
{N.j where j is Element of N : a <= j} c= the carrier of T
proof
let q be object;
assume q in {N.j where j is Element of N : a <= j};
then ex j being Element of N st q = N.j & a <= j;
hence thesis;
end;
then reconsider
X = {N.j where j is Element of N : a <= j} as Subset of the
carrier of T;
take Cl X, X, a;
thus thesis;
end;
consider F being Function of the carrier of N, bool the carrier of T such
that
A2: for e being Element of N holds P[e,F.e] from FUNCT_2:sch 3(A1);
reconsider RF = rng F as Subset-Family of T;
A3: dom F = the carrier of N by FUNCT_2:def 1;
A4: RF is centered
proof
thus RF <> {} by A3,RELAT_1:42;
defpred P[set,set] means ex i being Element of N, h, Ch being Subset of T
st i = $2 & Ch = $1 & h = {N.j where j is Element of N : i <= j} & Ch = Cl h;
set J = {i where i is Element of N : ex h, Ch being Subset of T st h = {N.
j where j is Element of N : i <= j} & Ch = Cl h};
let H be set such that
A5: H <> {} and
A6: H c= RF and
A7: H is finite;
reconsider H1 = H as non empty set by A5;
set e = the Element of H1;
e in RF by A6;
then consider x being object such that
A8: x in dom F and
e = F.x by FUNCT_1:def 3;
reconsider x as Element of N by A8;
consider X being Subset of T, a being Element of N such that
a = x and
A9: X = {N.j where j is Element of N : a <= j} & F.x = Cl X by A2;
a in J by A9;
then reconsider J as non empty set;
A10: for e being Element of H1 ex u being Element of J st P[e,u]
proof
let e be Element of H1;
e in RF by A6;
then consider x being object such that
A11: x in dom F and
A12: e = F.x by FUNCT_1:def 3;
reconsider x as Element of N by A11;
consider X being Subset of T, a being Element of N such that
A13: a = x and
A14: X = {N.j where j is Element of N : a <= j} and
A15: F.x = Cl X by A2;
a in J by A14,A15;
then reconsider a as Element of J;
take u = a, i = x, h = X, Ch = Cl X;
thus i = u by A13;
thus Ch = e by A12,A15;
thus h = {N.j where j is Element of N : i <= j} by A13,A14;
thus thesis;
end;
consider Q being Function of H1, J such that
A16: for e being Element of H1 holds P[e,Q.e] from FUNCT_2:sch 3(A10);
rng Q c= [#]N
proof
let q be object;
assume q in rng Q;
then consider x being object such that
A17: x in dom Q and
A18: Q.x = q by FUNCT_1:def 3;
reconsider x as Element of H1 by A17;
ex i being Element of N, h, Ch being Subset of T st i = Q .x & Ch =
x & h = {N.j where j is Element of N : i <= j} & Ch = Cl h by A16;
hence thesis by A18;
end;
then reconsider RQ = rng Q as Subset of [#]N;
A19: [#]N is non empty directed by WAYBEL_0:def 6;
dom Q = H by FUNCT_2:def 1;
then rng Q is finite by A7,FINSET_1:8;
then consider i0 being Element of N such that
i0 in [#]N and
A20: i0 is_>=_than RQ by A19,WAYBEL_0:1;
for Y being set holds Y in H implies N.i0 in Y
proof
let Y be set;
assume
A21: Y in H;
then consider i being Element of N, h, Ch being Subset of T such that
A22: i = Q.Y and
A23: Ch = Y and
A24: h = {N.j where j is Element of N : i <= j} and
A25: Ch = Cl h by A16;
Y in dom Q by A21,FUNCT_2:def 1;
then i in rng Q by A22,FUNCT_1:def 3;
then i <= i0 by A20;
then
A26: N.i0 in h by A24;
h c= Cl h by PRE_TOPC:18;
hence thesis by A23,A25,A26;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
RF is closed
proof
let P be Subset of T;
assume P in RF;
then consider x being object such that
A27: x in dom F and
A28: F.x = P by FUNCT_1:def 3;
reconsider x as Element of N by A27;
ex X being Subset of T, a being Element of N st a = x & X = {N.j where
j is Element of N : a <= j} & F.x = Cl X by A2;
then P = Cl P by A28;
hence thesis;
end;
then meet RF <> {} by A4,COMPTS_1:4;
then consider c being object such that
A29: c in meet RF by XBOOLE_0:def 1;
reconsider c as Point of T by A29;
take c;
assume not c is_a_cluster_point_of N;
then consider O being a_neighborhood of c such that
A30: not N is_often_in O;
N is_eventually_in (the carrier of T) \ O by A30,WAYBEL_0:10;
then consider s0 being Element of N such that
A31: for j being Element of N st s0 <= j holds N.j in (the carrier of T)
\ O;
consider Y being Subset of T, a being Element of N such that
A32: a = s0 & Y = {N.j where j is Element of N : a <= j} and
A33: F.s0 = Cl Y by A2;
Cl Y in RF by A3,A33,FUNCT_1:def 3;
then
A34: c in Cl Y by A29,SETFAM_1:def 1;
{} = O /\ Y
proof
thus {} c= O /\ Y;
let q be object such that
A35: q in O /\ Y;
q in Y by A35,XBOOLE_0:def 4;
then consider j being Element of N such that
A36: q = N.j and
A37: s0 <= j by A32;
assume not q in {};
N.j in (the carrier of T) \ O by A31,A37;
then not N.j in O by XBOOLE_0:def 5;
hence contradiction by A35,A36,XBOOLE_0:def 4;
end;
then O misses Y;
then
A38: Int O misses Y by TOPS_1:16,XBOOLE_1:63;
Int O is open & c in Int O by CONNSP_2:def 1;
hence contradiction by A34,A38,PRE_TOPC:def 7;
end;
theorem Th31:
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
by YELLOW_6:18;
theorem Th32:
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
proof
let T be non empty TopSpace, N be net of T, x be Point of T such that
A1: x is_a_cluster_point_of N;
set q = the Element of N;
set S9 = {[s,O] where s is Element of N, O is Element of OpenNeighborhoods x
: N.s in O};
reconsider O = [#]T as Element of OpenNeighborhoods x by YELLOW_6:30;
N.q in [#]T;
then [q,O] in S9;
then reconsider S9 as non empty set;
set n = the mapping of N;
defpred P[set,set] means ex s1, s2 being Element of N st s1 = $1`1 & s2 = $2
`1 & s1 <= s2 & $2`2 c= $1`2;
consider L being non empty strict RelStr such that
A2: the carrier of L = S9 and
A3: for a, b being Element of L holds a <= b iff P[a,b] from YELLOW_0:
sch 1;
deffunc F(Element of L) = n.($1`1);
A4: for a being Element of L holds F(a) in the carrier of T
proof
let a be Element of L;
a in S9 by A2;
then consider
s being Element of N, O being Element of OpenNeighborhoods x such
that
A5: a = [s,O] and
N.s in O;
n.(a`1) = n.s by A5;
hence thesis;
end;
consider g being Function of the carrier of L, the carrier of T such that
A6: for x being Element of L holds g.x = F(x) from FUNCT_2:sch 8(A4);
set M = NetStr (#the carrier of L, the InternalRel of L, g#);
for a, b being Element of M ex z being Element of M st a <= z & b <= z
proof
let a, b be Element of M;
a in S9 by A2;
then consider
aa being Element of N, Oa being Element of OpenNeighborhoods x
such that
A7: a = [aa,Oa] and
N.aa in Oa;
b in S9 by A2;
then consider
bb being Element of N, Ob being Element of OpenNeighborhoods x
such that
A8: b = [bb,Ob] and
N.bb in Ob;
consider z1 being Element of N such that
A9: aa <= z1 and
A10: bb <= z1 by YELLOW_6:def 3;
Oa is a_neighborhood of x & Ob is a_neighborhood of x by Th21;
then Oa /\ Ob is a_neighborhood of x by CONNSP_2:2;
then N is_often_in Oa /\ Ob by A1;
then consider d being Element of N such that
A11: z1 <= d and
A12: N.d in Oa /\ Ob;
Oa /\ Ob is Element of OpenNeighborhoods x by Th22;
then [d, Oa /\ Ob] in S9 by A12;
then reconsider z = [d, Oa /\ Ob] as Element of M by A2;
reconsider A1 = a, C7 = b, z2 = z as Element of L;
A13: C7`1 = bb & C7`2 = Ob by A8;
take z;
A14: A1`1 = aa & A1`2 = Oa by A7;
A15: z2`1 = d & z2`2 = Oa /\ Ob;
Oa /\ Ob c= Ob & bb <= d by A10,A11,XBOOLE_1:17,YELLOW_0:def 2;
then
A16: C7 <= z2 by A3,A13,A15;
Oa /\ Ob c= Oa & aa <= d by A9,A11,XBOOLE_1:17,YELLOW_0:def 2;
then A1 <= z2 by A3,A14,A15;
hence thesis by A16;
end;
then reconsider M as prenet of T by YELLOW_6:def 3;
M is transitive
proof
let x, y, z be Element of M such that
A17: x <= y and
A18: y <= z;
reconsider x1 = x, y1 = y, z1 = z as Element of L;
x1 <= y1 by A17;
then consider sx, sy being Element of N such that
A19: sx = x1`1 and
A20: sy = y1`1 & sx <= sy & y1`2 c= x1`2 by A3;
y1 <= z1 by A18;
then consider s1, s2 being Element of N such that
A21: s1 = y1`1 and
A22: s2 = z1`1 and
A23: s1 <= s2 & z1`2 c= y1`2 by A3;
sx <= s2 & z1`2 c= x1`2 by A20,A21,A23,YELLOW_0:def 2;
then x1 <= z1 by A3,A19,A22;
hence thesis;
end;
then reconsider M as net of T;
M is subnet of N
proof
deffunc F(Element of L) = $1`1;
A24: for a being Element of L holds F(a) in the carrier of N
proof
let a be Element of L;
a in S9 by A2;
then consider
s being Element of N, O being Element of OpenNeighborhoods x
such that
A25: a = [s,O] and
N.s in O;
a`1 = s by A25;
hence thesis;
end;
consider f being Function of the carrier of L, the carrier of N such that
A26: for x being Element of L holds f.x = F(x) from FUNCT_2:sch 8(A24);
reconsider f as Function of M, N;
take f;
for x being object st x in the carrier of M holds g.x = (n*f).x
proof
let x be object;
assume
A27: x in the carrier of M;
hence g.x = n.(x`1) by A6
.= n.(f.x) by A26,A27
.= (n*f).x by A27,FUNCT_2:15;
end;
hence the mapping of M = (the mapping of N)*f by FUNCT_2:12;
let m be Element of N;
N.m in [#]T;
then [m,O] in S9;
then reconsider n = [m,O] as Element of M by A2;
take n;
let p be Element of M such that
A28: n <= p;
reconsider n1 = n, p1 = p as Element of L;
n1 <= p1 by A28;
then
A29: ex s1, s2 being Element of N st s1 = n1`1 & s2 = p1`1 & s1 <= s2 & p1
`2 c= n1`2 by A3;
f.p = p`1 by A26;
hence thesis by A29;
end;
then reconsider M as subnet of N;
take M;
for V being a_neighborhood of x holds M is_eventually_in V
proof
set i = the Element of N;
let V be a_neighborhood of x;
x in Int V & Int V is open by CONNSP_2:def 1;
then
A30: Int V in the carrier of OpenNeighborhoods x by YELLOW_6:30;
then Int V is a_neighborhood of x by Th21;
then N is_often_in Int V by A1;
then consider s being Element of N such that
i <= s and
A31: N.s in Int V;
A32: M is_eventually_in Int V
proof
[s,Int V] in S9 by A30,A31;
then reconsider j = [s,Int V] as Element of M by A2;
take j;
let s9 be Element of M such that
A33: j <= s9;
reconsider j1 = j, s1 = s9 as Element of L;
j1 <= s1 by A33;
then
A34: ex s1, s2 being Element of N st s1 = j`1 & s2 = s9`1 & s1 <= s2 & s9
`2 c= j`2 by A3;
s9 in S9 by A2;
then consider
ss being Element of N, OO being Element of OpenNeighborhoods x
such that
A35: s9 = [ss,OO] and
A36: N.ss in OO;
A37: j`2 = Int V & s9`2 = OO by A35;
M.s9 = n.(s9`1) by A6
.= N.ss by A35;
hence thesis by A36,A34,A37;
end;
Int V c= V by TOPS_1:16;
hence thesis by A32,WAYBEL_0:8;
end;
hence thesis by YELLOW_6:def 15;
end;
theorem Th33:
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
proof
let L be compact Hausdorff non empty TopSpace, N be net of L such that
A1: 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;
let c be Point of L such that
A2: c is_a_cluster_point_of N;
assume not c in Lim N;
then consider M being subnet of N such that
A3: not ex P being subnet of M st c in Lim P by YELLOW_6:37;
consider d being Point of L such that
A4: d is_a_cluster_point_of M by Th30;
A5: d is_a_cluster_point_of N by A4,Th31;
c <> d by A3,A4,Th32;
hence contradiction by A1,A2,A5;
end;
theorem Th34:
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
proof
let S be non empty TopSpace, c be Point of S, N be net of S, A be Subset of
S such that
A1: c is_a_cluster_point_of N and
A2: A is closed and
A3: rng the mapping of N c= A;
consider M being subnet of N such that
A4: c in Lim M by A1,Th32;
reconsider R = rng the mapping of M as Subset of S;
ex f being Function of M, N st the mapping of M = (the mapping of N)*f &
for m being Element of N ex n being Element of M st for p being Element of M st
n <= p holds m <= f.p by YELLOW_6:def 9;
then R c= rng the mapping of N by RELAT_1:26;
then R c= A by A3;
then
A5: Cl R c= Cl A by PRE_TOPC:19;
c in Cl R by A4,Th24;
then c in Cl A by A5;
hence thesis by A2,PRE_TOPC:22;
end;
Lm5: for S being compact Hausdorff TopLattice, N being net of S for c being
Point of S, d being Element of S st c = d & (for x being Element of S holds x
"/\" is continuous) & N is eventually-directed & c is_a_cluster_point_of N
holds d is_>=_than rng the mapping of N
proof
let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be
Element of S such that
A1: c = d and
A2: for x being Element of S holds x"/\" is continuous and
A3: N is eventually-directed and
A4: c is_a_cluster_point_of N;
let i be Element of S;
assume i in rng the mapping of N;
then consider iJ being object such that
A5: iJ in dom the mapping of N and
A6: (the mapping of N).iJ = i by FUNCT_1:def 3;
reconsider i1 = iJ as Element of N by A5;
uparrow N.i1 is closed by A2,Th27;
then
A7: Cl (uparrow N.i1) = uparrow N.i1 by PRE_TOPC:22;
N is_eventually_in uparrow (N.i1)
proof
consider j being Element of N such that
A8: for k being Element of N st j <= k holds N.i1 <= N.k by A3,WAYBEL_0:11;
take j;
let k be Element of N;
assume j <= k;
then N.i1 <= N.k by A8;
hence thesis by WAYBEL_0:18;
end;
then consider t being Element of N such that
A9: for j being Element of N st t <= j holds N.j in uparrow N.i1;
reconsider A = N|t as subnet of N;
A10: rng the mapping of A c= uparrow N.i1
proof
let q be object;
assume q in rng the mapping of A;
then consider x being object such that
A11: x in dom the mapping of A and
A12: q = (the mapping of A).x by FUNCT_1:def 3;
reconsider x as Element of A by A11;
consider y being Element of N such that
A13: y = x and
A14: t <= y by Def7;
A.x = N.y by A13,Th16;
hence thesis by A9,A12,A14;
end;
c is_a_cluster_point_of A
proof
let O be a_neighborhood of c;
let i be Element of A;
consider i2 being Element of N such that
A15: i2 = i and
A16: t <= i2 by Def7;
N is_often_in O by A4;
then consider j2 being Element of N such that
A17: i2 <= j2 and
A18: N.j2 in O;
t <= j2 by A16,A17,YELLOW_0:def 2;
then reconsider j = j2 as Element of A by Def7;
take j;
A is full SubNetStr of N by Th14;
hence i <= j by A15,A17,YELLOW_6:12;
thus thesis by A18,Th16;
end;
then consider M being subnet of A such that
A19: c in Lim M by Th32;
reconsider R = rng the mapping of M as Subset of S;
A20: uparrow (N.i1) = {z where z is Element of S : z "/\" N.i1 = N.i1} by Lm1;
ex f being Function of M, A st the mapping of M = (the mapping of A)*f &
for m being Element of A ex n being Element of M st for p being Element of M st
n <= p holds m <= f.p by YELLOW_6:def 9;
then R c= rng the mapping of A by RELAT_1:26;
then R c= uparrow N.i1 by A10;
then
A21: Cl R c= Cl (uparrow N.i1) by PRE_TOPC:19;
c in Cl R by A19,Th24;
then c in uparrow (N.i1) by A7,A21;
then ex z being Element of S st c = z & z "/\" N.i1 = N.i1 by A20;
hence thesis by A1,A6,YELLOW_0:25;
end;
Lm6: for S being compact Hausdorff TopLattice, N being net of S for c being
Point of S, d being Element of S st c = d & (for x being Element of S holds x
"/\" is continuous) & c is_a_cluster_point_of N holds for b being Element of S
st rng the mapping of N is_<=_than b holds d <= b
proof
let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be
Element of S such that
A1: c = d and
A2: for x being Element of S holds x"/\" is continuous and
A3: c is_a_cluster_point_of N;
let b be Element of S such that
A4: rng the mapping of N is_<=_than b;
A5: now
let i be Element of N;
A6: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
N.i in rng the mapping of N by A6,FUNCT_1:def 3;
then N.i <= b by A4;
then
A7: b "/\" N.i = N.i by YELLOW_0:25;
b in {b} by TARSKI:def 1;
hence N.i in {b} "/\" [#]S by A7,YELLOW_4:37;
end;
A8: rng the mapping of N c= {b} "/\" [#]S
proof
let y be object;
assume y in rng the mapping of N;
then consider x being object such that
A9: x in dom the mapping of N and
A10: y = (the mapping of N).x by FUNCT_1:def 3;
reconsider x as Element of N by A9;
y = N.x by A10;
hence thesis by A5;
end;
downarrow b is closed by A2,Th28;
then {b} "/\" [#]S is closed by Th5;
then
{b} "/\" [#]S = {b "/\" y where y is Element of S: y in [#] S} & c in {
b} "/\" [#]S by A3,A8,Th34,YELLOW_4:42;
then ex y being Element of S st c = b "/\" y & y in [#]S;
hence thesis by A1,YELLOW_0:23;
end;
theorem Th35:
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
proof
let S be compact Hausdorff TopLattice, c be Point of S, N be net of S such
that
A1: ( for x being Element of S holds x"/\" is continuous)& N is
eventually-directed & c is_a_cluster_point_of N;
reconsider c9 = c as Element of S;
c9 is_>=_than rng the mapping of N & for b being Element of S st rng the
mapping of N is_<=_than b holds c9 <= b by A1,Lm5,Lm6;
hence c = sup rng the mapping of N by YELLOW_0:30
.= sup N by YELLOW_2:def 5;
end;
Lm7: for S being compact Hausdorff TopLattice, N being net of S for c being
Point of S, d being Element of S st c = d & (for x being Element of S holds x
"/\" is continuous) & N is eventually-filtered & c is_a_cluster_point_of N
holds d is_<=_than rng the mapping of N
proof
let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be
Element of S such that
A1: c = d and
A2: for x being Element of S holds x"/\" is continuous and
A3: N is eventually-filtered and
A4: c is_a_cluster_point_of N;
let i be Element of S;
assume i in rng the mapping of N;
then consider iJ being object such that
A5: iJ in dom the mapping of N and
A6: (the mapping of N).iJ = i by FUNCT_1:def 3;
reconsider i1 = iJ as Element of N by A5;
downarrow N.i1 is closed by A2,Th28;
then
A7: Cl (downarrow N.i1) = downarrow N.i1 by PRE_TOPC:22;
N is_eventually_in downarrow (N.i1)
proof
consider j being Element of N such that
A8: for k being Element of N st j <= k holds N.i1 >= N.k by A3,WAYBEL_0:12;
take j;
let k be Element of N;
assume j <= k;
then N.i1 >= N.k by A8;
hence thesis by WAYBEL_0:17;
end;
then consider t being Element of N such that
A9: for j being Element of N st t <= j holds N.j in downarrow N.i1;
reconsider A = N|t as subnet of N;
A10: rng the mapping of A c= downarrow N.i1
proof
let q be object;
assume q in rng the mapping of A;
then consider x being object such that
A11: x in dom the mapping of A and
A12: q = (the mapping of A).x by FUNCT_1:def 3;
reconsider x as Element of A by A11;
consider y being Element of N such that
A13: y = x and
A14: t <= y by Def7;
A.x = N.y by A13,Th16;
hence thesis by A9,A12,A14;
end;
c is_a_cluster_point_of A
proof
let O be a_neighborhood of c;
let i be Element of A;
consider i2 being Element of N such that
A15: i2 = i and
A16: t <= i2 by Def7;
N is_often_in O by A4;
then consider j2 being Element of N such that
A17: i2 <= j2 and
A18: N.j2 in O;
t <= j2 by A16,A17,YELLOW_0:def 2;
then reconsider j = j2 as Element of A by Def7;
take j;
A is full SubNetStr of N by Th14;
hence i <= j by A15,A17,YELLOW_6:12;
thus thesis by A18,Th16;
end;
then consider M being subnet of A such that
A19: c in Lim M by Th32;
reconsider R = rng the mapping of M as Subset of S;
A20: downarrow (N.i1) = {z where z is Element of S : z "\/" N.i1 = N.i1} by Lm2
;
ex f being Function of M, A st the mapping of M = (the mapping of A)*f &
for m being Element of A ex n being Element of M st for p being Element of M st
n <= p holds m <= f.p by YELLOW_6:def 9;
then R c= rng the mapping of A by RELAT_1:26;
then R c= downarrow N.i1 by A10;
then
A21: Cl R c= Cl (downarrow N.i1) by PRE_TOPC:19;
c in Cl R by A19,Th24;
then c in downarrow (N.i1) by A7,A21;
then ex z being Element of S st c = z & z "\/" N.i1 = N.i1 by A20;
hence d <= i by A1,A6,YELLOW_0:24;
end;
Lm8: for S being compact Hausdorff TopLattice, N being net of S for c being
Point of S, d being Element of S st c = d & (for x being Element of S holds x
"/\" is continuous) & c is_a_cluster_point_of N holds for b being Element of S
st rng the mapping of N is_>=_than b holds d >= b
proof
let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be
Element of S such that
A1: c = d and
A2: for x being Element of S holds x"/\" is continuous and
A3: c is_a_cluster_point_of N;
let b be Element of S such that
A4: rng the mapping of N is_>=_than b;
A5: now
let i be Element of N;
A6: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
N.i in rng the mapping of N by A6,FUNCT_1:def 3;
then N.i >= b by A4;
then
A7: b "\/" N.i = N.i by YELLOW_0:24;
b in {b} by TARSKI:def 1;
hence N.i in {b} "\/" [#]S by A7,YELLOW_4:10;
end;
A8: rng the mapping of N c= {b} "\/" [#]S
proof
let y be object;
assume y in rng the mapping of N;
then consider x being object such that
A9: x in dom the mapping of N and
A10: y = (the mapping of N).x by FUNCT_1:def 3;
reconsider x as Element of N by A9;
y = N.x by A10;
hence thesis by A5;
end;
uparrow b is closed by A2,Th27;
then {b} "\/" [#]S is closed by Th4;
then
{b} "\/" [#]S = {b "\/" y where y is Element of S: y in [#] S} & c in {
b} "\/" [#]S by A3,A8,Th34,YELLOW_4:15;
then ex y being Element of S st c = b "\/" y & y in [#]S;
hence thesis by A1,YELLOW_0:22;
end;
theorem Th36:
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
proof
let S be compact Hausdorff TopLattice, c be Point of S, N be net of S such
that
A1: ( for x being Element of S holds x"/\" is continuous)& N is
eventually-filtered & c is_a_cluster_point_of N;
reconsider c9 = c as Element of S;
c9 is_<=_than rng the mapping of N & for b being Element of S st rng the
mapping of N is_>=_than b holds c9 >= b by A1,Lm7,Lm8;
hence c = inf rng the mapping of N by YELLOW_0:31
.= inf N by YELLOW_2:def 6;
end;
begin :: On The Topological Properties of Meet-Continuous Lattices
:: Proposition 4.4 s. 32 (i) & (ii) => MC
theorem Th37:
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
proof
let S be Hausdorff TopLattice such that
A1: for N being net of S st N is eventually-directed holds ex_sup_of N &
sup N in Lim N and
A2: for x being Element of S holds x "/\" is continuous;
for X being non empty directed Subset of S holds ex_sup_of X,S
proof
let X be non empty directed Subset of S;
reconsider n = id X as Function of X, the carrier of S by FUNCT_2:7;
set N = NetStr (#X,(the InternalRel of S)|_2 X,n#);
N is eventually-directed by WAYBEL_2:20;
then
A3: ex_sup_of N by A1;
rng the mapping of N = X by RELAT_1:45;
hence thesis by A3;
end;
hence S is up-complete by WAYBEL_0:75;
for x being Element of S, M being net of S st M is eventually-directed
holds x "/\" sup M = sup ({x} "/\" rng netmap (M,S))
proof
let x be Element of S, M be net of S such that
A4: M is eventually-directed;
A5: sup M in Lim M by A1,A4;
then reconsider M1 = M as convergent net of S by YELLOW_6:def 16;
set xM = x "/\" M;
x "/\" M is eventually-directed by A4,WAYBEL_2:27;
then
A6: sup xM in Lim xM by A1;
x"/\" is continuous by A2;
then
A7: x "/\" lim M1 in Lim (x "/\" M1) by Th26;
reconsider xM as convergent net of S by A6,YELLOW_6:def 16;
thus x "/\" sup M = x "/\" lim M1 by A5,YELLOW_6:def 17
.= lim xM by A7,YELLOW_6:def 17
.= Sup the mapping of xM by A6,YELLOW_6:def 17
.= sup rng the mapping of xM by YELLOW_2:def 5
.= sup ({x} "/\" rng netmap (M,S)) by WAYBEL_2:23;
end;
hence thesis by Th9;
end;
:: Proposition 4.4 s. 32 (ii) => (i)
theorem Th38:
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
proof
let S be compact Hausdorff TopLattice such that
A1: for x being Element of S holds x "/\" is continuous;
let N be net of S such that
A2: N is eventually-directed;
A3: for c, d being Point of S st c is_a_cluster_point_of N & d
is_a_cluster_point_of N holds c = d
proof
let c, d be Point of S such that
A4: c is_a_cluster_point_of N and
A5: d is_a_cluster_point_of N;
thus c = sup N by A1,A2,A4,Th35
.= d by A1,A2,A5,Th35;
end;
consider c being Point of S such that
A6: c is_a_cluster_point_of N by Th30;
thus ex_sup_of N
proof
reconsider d = c as Element of S;
set X = rng the mapping of N;
X is_<=_than d & for b being Element of S st X is_<=_than b holds d <=
b by A1,A2,A6,Lm5,Lm6;
hence ex_sup_of rng the mapping of N, S by YELLOW_0:15;
end;
c = sup N by A1,A2,A6,Th35;
hence thesis by A6,A3,Th33;
end;
:: Proposition 4.4 s. 32 (ii) => (i) dual
theorem Th39:
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
proof
let S be compact Hausdorff TopLattice such that
A1: for x being Element of S holds x "/\" is continuous;
let N be net of S such that
A2: N is eventually-filtered;
A3: for c, d being Point of S st c is_a_cluster_point_of N & d
is_a_cluster_point_of N holds c = d
proof
let c, d be Point of S such that
A4: c is_a_cluster_point_of N and
A5: d is_a_cluster_point_of N;
thus c = inf N by A1,A2,A4,Th36
.= d by A1,A2,A5,Th36;
end;
consider c being Point of S such that
A6: c is_a_cluster_point_of N by Th30;
thus ex_inf_of N
proof
reconsider d = c as Element of S;
set X = rng the mapping of N;
X is_>=_than d & for b being Element of S st X is_>=_than b holds d >=
b by A1,A2,A6,Lm7,Lm8;
hence ex_inf_of rng the mapping of N, S by YELLOW_0:16;
end;
c = inf N by A1,A2,A6,Th36;
hence thesis by A6,A3,Th33;
end;
theorem
for S being compact Hausdorff TopLattice st for x being Element of S
holds x"/\" is continuous holds S is bounded
proof
let S be compact Hausdorff TopLattice such that
A1: for x being Element of S holds x"/\" is continuous;
thus S is lower-bounded
proof
reconsider x = inf (S opp+id) as Element of S;
take x;
A2: rng the mapping of S opp+id = rng id S by Def6
.= the carrier of S by RELAT_1:45;
then
A3: x = "/\"(the carrier of S,S) by YELLOW_2:def 6;
ex_inf_of S opp+id by A1,Th39;
then ex_inf_of the carrier of S, S by A2;
hence thesis by A3,YELLOW_0:31;
end;
reconsider x = sup (S+id) as Element of S;
take x;
A4: rng the mapping of S+id = rng id S by Def5
.= the carrier of S by RELAT_1:45;
then
A5: x = "\/"(the carrier of S,S) by YELLOW_2:def 5;
ex_sup_of S+id by A1,Th38;
then ex_sup_of the carrier of S, S by A4;
hence thesis by A5,YELLOW_0:30;
end;
theorem
for S being compact Hausdorff TopLattice st for x being Element of S
holds x"/\" is continuous holds S is meet-continuous
proof
let S be compact Hausdorff TopLattice;
assume
A1: for x being Element of S holds x "/\" is continuous;
then
for N being net of S st N is eventually-directed holds ex_sup_of N & sup
N in Lim N by Th38;
hence thesis by A1,Th37;
end;