:: The Lawson Topology
:: by Grzegorz Bancerek
::
:: Received June 21, 1998
:: Copyright (c) 1998-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, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, ORDERS_2,
ZFMISC_1, RELAT_2, PRE_TOPC, STRUCT_0, RLVECT_3, TARSKI, SETFAM_1,
XXREAL_0, REWRITE1, PRELAMB, YELLOW_9, ORDINAL1, RCOMP_1, FINSET_1,
FUNCT_1, RELAT_1, ORDINAL2, YELLOW_0, LATTICES, CAT_1, ARYTM_0, LATTICE3,
SEQM_3, WAYBEL_2, WAYBEL_3, CONNSP_2, TOPS_1, PROB_1, WAYBEL11, DIRAF,
CARD_FIL, YELLOW_1, EQREL_1, COMPTS_1, WAYBEL19, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FINSET_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3,
ORDERS_3, PRE_TOPC, TOPS_1, CONNSP_2, BORSUK_1, COMPTS_1, YELLOW_0,
WAYBEL_0, YELLOW_1, CANTOR_1, YELLOW_3, WAYBEL_2, YELLOW_6, YELLOW_7,
WAYBEL_3, WAYBEL_9, WAYBEL11, YELLOW_9;
constructors TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3, CANTOR_1, ORDERS_3,
WAYBEL_3, WAYBEL11, YELLOW_9, COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, BORSUK_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, YELLOW_6,
WAYBEL11, YELLOW_9, YELLOW12, TOPS_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_3,
WAYBEL11, YELLOW_9, XBOOLE_0;
equalities LATTICE3, WAYBEL_0, WAYBEL_3, SUBSET_1, STRUCT_0;
expansions TARSKI, PRE_TOPC, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL11,
XBOOLE_0;
theorems STRUCT_0, ENUMSET1, SUBSET_1, SETFAM_1, PRE_TOPC, CANTOR_1, YELLOW_0,
WAYBEL_0, FUNCT_1, RELAT_1, FUNCT_2, FINSET_1, BORSUK_1, CONNSP_2,
ORDERS_2, YELLOW_2, ZFMISC_1, TARSKI, YELLOW_6, TOPS_1, TOPS_2, TEX_2,
YELLOW_1, TSP_1, MSSUBFAM, WAYBEL_3, YELLOW_5, WAYBEL_7, LATTICE3,
YELLOW_3, YELLOW_7, YELLOW_8, WAYBEL_9, URYSOHN1, WAYBEL11, YELLOW_9,
YELLOW10, WAYBEL14, YELLOW12, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, FINSET_1, YELLOW_9, FUNCT_1;
begin :: Lower topoplogy
definition :: 1.1. DEFINITION, p. 142 (part I)
let T be non empty TopRelStr;
attr T is lower means
: Def1:
the set of all (uparrow x)` where x is Element of T is prebasis of T;
end;
Lm1: now
let LL,T be non empty RelStr such that
A1: the RelStr of LL = the RelStr of T;
set BB = the set of all (uparrow x)` where x is Element of T;
set A = the set of all (uparrow x)` where x is Element of LL;
thus A = BB
proof
hereby
let a be object;
assume a in A;
then consider x being Element of LL such that
A2: a = (uparrow x)`;
reconsider y = x as Element of T by A1;
a = (uparrow y)` by A1,A2,WAYBEL_0:13;
hence a in BB;
end;
let a be object;
assume a in BB;
then consider x being Element of T such that
A3: a = (uparrow x)`;
reconsider y = x as Element of LL by A1;
a = (uparrow y)` by A1,A3,WAYBEL_0:13;
hence thesis;
end;
end;
registration
cluster -> lower for 1-element reflexive TopSpace-like TopRelStr;
coherence
proof
let T be 1-element reflexive TopSpace-like TopRelStr;
set BB = the set of all (uparrow x)` where x is Element of T;
reconsider F = {the carrier of T} as Basis of T by YELLOW_9:10;
BB c= bool the carrier of T
proof
let a be object;
assume a in BB;
then ex x being Element of T st a = (uparrow x)`;
hence thesis;
end;
then reconsider C = BB as Subset-Family of T;
reconsider C as Subset-Family of T;
BB = {{}}
proof
set x = the Element of T;
thus BB c= {{}}
proof
let a be object;
assume a in BB;
then consider x being Element of T such that
A1: a = (uparrow x)`;
x <= x;
then
A2: x in uparrow x by WAYBEL_0:18;
the carrier of T = {x} by YELLOW_9:9;
then a = {} or a = the carrier of T & not x in (uparrow x)` by A2,A1,
XBOOLE_0:def 5,ZFMISC_1:33;
hence thesis by TARSKI:def 1,A1;
end;
x <= x;
then
A3: x in uparrow x by WAYBEL_0:18;
the carrier of T = {x} by YELLOW_9:9;
then (uparrow x)` = {} or (uparrow x)` = the carrier of T & not x in (
uparrow x)` by A3,XBOOLE_0:def 5,ZFMISC_1:33;
then {} in BB;
hence thesis by ZFMISC_1:31;
end;
then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
then
A4: F c= FinMeetCl C by ZFMISC_1:7;
BB c= the topology of T
proof
let a be object;
assume a in BB;
then consider x being Element of T such that
A5: a = (uparrow x)`;
(uparrow x)` c= {}
proof
let y be object;
x <= x;
then
A6: x in uparrow x by WAYBEL_0:18;
A7: (uparrow x) misses (uparrow x)` by XBOOLE_1:79;
assume
A8: y in (uparrow x)`;
then y = x by STRUCT_0:def 10;
then x in (uparrow x) /\ (uparrow x)` by A6,A8,XBOOLE_0:def 4;
hence thesis by A7;
end;
then a = {} by A5;
hence thesis by PRE_TOPC:1;
end;
hence BB is prebasis of T by A4,CANTOR_1:def 4,TOPS_2:64;
end;
end;
registration
cluster lower trivial complete strict for TopLattice;
existence
proof
set T = the 1-element complete strict TopLattice;
take T;
thus thesis;
end;
end;
theorem Th1:
for LL being non empty RelStr ex T being strict correct
TopAugmentation of LL st T is lower
proof
let LL be non empty RelStr;
set A = the set of all (uparrow x)` where x is Element of LL;
A c= bool the carrier of LL
proof
let a be object;
assume a in A;
then ex x being Element of LL st a = (uparrow x)`;
hence thesis;
end;
then reconsider A as Subset-Family of LL;
set T = TopRelStr(#the carrier of LL, the InternalRel of LL, UniCl FinMeetCl
A#);
reconsider S = TopStruct(#the carrier of LL, UniCl FinMeetCl A#) as non
empty TopSpace by CANTOR_1:15;
A1: the TopStruct of T = S;
T is TopSpace-like
by A1,PRE_TOPC:def 1;
then reconsider T as strict non empty TopSpace-like TopRelStr;
take T;
set BB = the set of all (uparrow x)` where x is Element of T;
the RelStr of T = the RelStr of LL;
hence T is strict correct TopAugmentation of LL by YELLOW_9:def 4;
A2: A is prebasis of S by CANTOR_1:18;
then consider F being Basis of S such that
A3: F c= FinMeetCl A by CANTOR_1:def 4;
A4: the topology of T c= UniCl F by CANTOR_1:def 2;
F c= the topology of T by TOPS_2:64;
then
A5: F is Basis of T by A4,CANTOR_1:def 2,TOPS_2:64;
the RelStr of T = the RelStr of LL;
then
A6: A = BB by Lm1;
A c= the topology of S by A2,TOPS_2:64;
hence BB is prebasis of T by A5,A3,A6,CANTOR_1:def 4,TOPS_2:64;
end;
registration
let R be non empty RelStr;
cluster lower for strict correct TopAugmentation of R;
existence by Th1;
end;
theorem Th2:
for L1,L2 being TopSpace-like lower non empty TopRelStr st the
RelStr of L1 = the RelStr of L2 holds the topology of L1 = the topology of L2
proof
let L1,L2 be TopSpace-like lower non empty TopRelStr such that
A1: the RelStr of L1 = the RelStr of L2;
set B2 = the set of all (uparrow x)` where x is Element of L2;
set B1 = the set of all (uparrow x)` where x is Element of L1;
A2: B1 is prebasis of L1 by Def1;
A3: B2 is prebasis of L2 by Def1;
B1 = B2 by A1,Lm1;
hence thesis by A1,A2,A3,YELLOW_9:26;
end;
definition :: 1.1. DEFINITION, p. 142 (part II)
let R be non empty RelStr;
func omega R -> Subset-Family of R means
: Def2:
for T being lower correct TopAugmentation of R holds it = the topology of T;
uniqueness
proof
set T = the lower correct TopAugmentation of R;
let X1,X2 be Subset-Family of R;
assume for T being lower correct TopAugmentation of R holds X1 = the
topology of T;
then X1 = the topology of T;
hence thesis;
end;
existence
proof
set S = the lower correct TopAugmentation of R;
A1: the RelStr of S = the RelStr of R by YELLOW_9:def 4;
then reconsider X = the topology of S as Subset-Family of R;
take X;
let T be lower correct TopAugmentation of R;
the RelStr of T = the RelStr of R by YELLOW_9:def 4;
hence thesis by A1,Th2;
end;
end;
theorem Th3:
for R1,R2 being non empty RelStr st the RelStr of R1 = the RelStr
of R2 holds omega R1 = omega R2
proof
let R1,R2 be non empty RelStr such that
A1: the RelStr of R1 = the RelStr of R2;
set S = the lower correct TopAugmentation of R1;
the RelStr of S = the RelStr of R1 by YELLOW_9:def 4;
then
A2: S is TopAugmentation of R2 by A1,YELLOW_9:def 4;
omega R1 = the topology of S by Def2;
hence thesis by A2,Def2;
end;
theorem Th4:
for T being lower non empty TopRelStr for x being Point of T
holds (uparrow x)` is open & uparrow x is closed
proof
let T be lower non empty TopRelStr;
set BB = the set of all (uparrow x)` where x is Element of T;
let x be Point of T;
reconsider a = x as Element of T;
BB is prebasis of T by Def1;
then
A1: BB c= the topology of T by TOPS_2:64;
A2: (uparrow a)` in BB;
hence (uparrow x)` in the topology of T by A1;
thus [#]T \ uparrow x in the topology of T by A2,A1;
end;
theorem Th5:
for T being transitive lower non empty TopRelStr for A being
Subset of T st A is open holds A is lower
proof
let T be transitive lower non empty TopRelStr;
reconsider BB = the set of all (uparrow x)` where x is Element of T as
prebasis of T by Def1;
let A be Subset of T such that
A1: A in the topology of T;
let x,y be Element of T;
consider F being Basis of T such that
A2: F c= FinMeetCl BB by CANTOR_1:def 4;
the topology of T c= UniCl F by CANTOR_1:def 2;
then consider Y being Subset-Family of T such that
A3: Y c= F and
A4: A = union Y by A1,CANTOR_1:def 1;
assume x in A;
then consider Z being set such that
A5: x in Z and
A6: Z in Y by A4,TARSKI:def 4;
Z in F by A3,A6;
then consider X being Subset-Family of T such that
A7: X c= BB and
X is finite and
A8: Z = Intersect X by A2,CANTOR_1:def 3;
assume
A9: x >= y;
now
let Q be set;
assume
A10: Q in X;
then Q in BB by A7;
then consider z being Element of T such that
A11: Q = (uparrow z)`;
(uparrow z) misses Q by A11,XBOOLE_1:79;
then
A12: (uparrow z) /\ Q = {}T;
x in Q by A5,A8,A10,SETFAM_1:43;
then not x in uparrow z by A12,XBOOLE_0:def 4;
then not x >= z by WAYBEL_0:18;
then not y >= z by A9,ORDERS_2:3;
then not y in uparrow z by WAYBEL_0:18;
hence y in Q by A11,XBOOLE_0:def 5;
end;
then y in Z by A8,SETFAM_1:43;
hence thesis by A4,A6,TARSKI:def 4;
end;
theorem Th6:
for T being transitive lower non empty TopRelStr for A being
Subset of T st A is closed holds A is upper
proof
let T be transitive lower non empty TopRelStr;
let A be Subset of T;
assume [#]T\A in the topology of T;
then A` is open;
then
A1: A` is lower by Th5;
let x,y be Element of T;
assume that
A2: x in A and
A3: x <= y and
A4: not y in A;
A5: y in A` by A4,XBOOLE_0:def 5;
not x in A` by A2,XBOOLE_0:def 5;
hence thesis by A5,A1,A3;
end;
theorem Th7:
for T being non empty TopSpace-like TopRelStr holds T is lower
iff {(uparrow F)` where F is Subset of T: F is finite} is Basis of T
proof
let T be non empty TopSpace-like TopRelStr;
set BB = the set of all (uparrow x)` where x is Element of T;
BB c= bool the carrier of T
proof
let x be object;
assume x in BB;
then ex y being Element of T st x = (uparrow y)`;
hence thesis;
end;
then reconsider BB as Subset-Family of T;
reconsider T9 = T as non empty RelStr;
set A = {(uparrow F)` where F is Subset of T: F is finite};
reconsider BB as Subset-Family of T;
A1: A = FinMeetCl BB
proof
deffunc F(Element of T9) = uparrow $1;
defpred P[object,object] means
ex x being Element of T st x = $2 & $1 = (uparrow x)`;
hereby
deffunc F(Element of T9) = uparrow $1;
let a be object;
assume a in A;
then consider F being Subset of T such that
A2: a = (uparrow F)` and
A3: F is finite;
set Y = {uparrow x where x is Element of T: x in F};
Y c= bool the carrier of T
proof
let a be object;
assume a in Y;
then ex x being Element of T st a = uparrow x & x in F;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
reconsider Y as Subset-Family of T;
uparrow F = union Y by YELLOW_9:4;
then
A4: a = Intersect COMPLEMENT Y by A2,YELLOW_8:6;
reconsider Y9 = Y as Subset-Family of T9;
A5: Y9 = {F(x) where x is Element of T9: x in F};
A6: COMPLEMENT Y9 = {F(x)` where x is Element of T9: x in F} from
YELLOW_9:sch 2(A5);
A7: COMPLEMENT Y c= BB
proof
let b be object;
assume b in COMPLEMENT Y;
then ex x being Element of T st b = (uparrow x)` & x in F by A6;
hence thesis;
end;
deffunc F(Element of T) = (uparrow $1)`;
{F(x) where x is Element of T: x in F} is finite from FRAENKEL:sch
21(A3);
hence a in FinMeetCl BB by A7,A6,A4,CANTOR_1:def 3;
end;
let a be object;
assume a in FinMeetCl BB;
then consider Y being Subset-Family of T such that
A8: Y c= BB and
A9: Y is finite and
A10: a = Intersect Y by CANTOR_1:def 3;
A11: now
let y be object;
assume y in Y;
then y in BB by A8;
then ex x being Element of T st y = (uparrow x)`;
hence ex b being object st b in the carrier of T & P[y,b];
end;
consider f being Function such that
A12: dom f = Y & rng f c= the carrier of T and
A13: for y being object st y in Y holds P[y,f.y] from FUNCT_1:sch 6(A11);
reconsider F = rng f as Subset of T by A12;
A14: F is finite by A9,A12,FINSET_1:8;
set X = {uparrow x where x is Element of T: x in F};
X c= bool the carrier of T
proof
let a be object;
assume a in X;
then ex x being Element of T st a = uparrow x & x in F;
hence thesis;
end;
then reconsider X as Subset-Family of T;
reconsider X as Subset-Family of T;
reconsider X9 = X as Subset-Family of T9;
A15: X9 = {F(x) where x is Element of T9: x in F};
A16: COMPLEMENT X9 = {F(x)` where x is Element of T9: x in F} from
YELLOW_9:sch 2(A15);
A17: COMPLEMENT X = Y
proof
hereby
let a be object;
assume a in COMPLEMENT X;
then consider x being Element of T9 such that
A18: a = (uparrow x)` and
A19: x in F by A16;
consider y being object such that
A20: y in Y and
A21: x = f.y by A12,A19,FUNCT_1:def 3;
ex z being Element of T st z = f.y & y = (uparrow z)` by A13,A20;
hence a in Y by A18,A20,A21;
end;
let a be object;
assume
A22: a in Y;
then consider z being Element of T such that
A23: z = f.a and
A24: a = (uparrow z)` by A13;
z in F by A12,A22,A23,FUNCT_1:def 3;
hence thesis by A16,A24;
end;
uparrow F = union X by YELLOW_9:4;
then a = (uparrow F)` by A10,A17,YELLOW_8:6;
hence thesis by A14;
end;
thus thesis by A1,YELLOW_9:23;
end;
theorem Th8:
:: 1.2. LEMMA, (i) generalized, p. 143
for S,T being lower complete TopLattice, f being Function of S, T
st for X being non empty Subset of S holds f preserves_inf_of X holds f is
continuous
proof
let S,T be lower complete non empty TopLattice;
reconsider BB = the set of all (uparrow x)` where x is Element of T as
prebasis of T by Def1;
let f be Function of S,T such that
A1: for X being non empty Subset of S holds f preserves_inf_of X;
now
let A be Subset of T;
A2: ex_inf_of f"A`, S by YELLOW_0:17;
A3: ex_inf_of A`, T by YELLOW_0:17;
A4: ex_inf_of f.:(f"A`), T by YELLOW_0:17;
assume A in BB;
then consider x being Element of T such that
A5: A = (uparrow x)`;
set s = inf (f"uparrow x);
per cases;
suppose
f"A` = {}S;
hence f"A` is closed;
end;
suppose
f"A` <> {};
then f preserves_inf_of f"A` by A1;
then
A6: f.s = inf (f.:(f"A`)) by A5,A2;
inf A` = x by A5,WAYBEL_0:39;
then
A7: x <= f.s by A6,A3,A4,FUNCT_1:75,YELLOW_0:35;
f"A` = uparrow s
proof
thus f"A` c= uparrow s
proof
let a be object;
assume
A8: a in f"A`;
then reconsider a as Element of S;
s <= a by A5,A8,YELLOW_2:22;
hence thesis by WAYBEL_0:18;
end;
let a be object;
assume
A9: a in uparrow s;
then reconsider a as Element of S;
f preserves_inf_of {s,a} by A1;
then
A10: f.(s"/\"a) = (f.s)"/\"(f.a) by YELLOW_3:8;
s <= a by A9,WAYBEL_0:18;
then f.s = (f.s)"/\"(f.a) by A10,YELLOW_5:10;
then f.s <= f.a by YELLOW_0:23;
then x <= f.a by A7,ORDERS_2:3;
then f.a in uparrow x by WAYBEL_0:18;
hence thesis by A5,FUNCT_2:38;
end;
hence f"A` is closed by Th4;
end;
end;
hence thesis by YELLOW_9:35;
end;
theorem Th9:
:: 1.2. LEMMA (i), p. 143
for S,T being lower complete TopLattice, f being Function of S, T
st f is infs-preserving holds f is continuous
proof
let S,T be lower complete non empty TopLattice;
let f be Function of S,T;
assume f is infs-preserving;
then for X being non empty Subset of S holds f preserves_inf_of X;
hence thesis by Th8;
end;
theorem Th10:
for T being lower complete TopLattice, BB being prebasis of T
for F being non empty filtered Subset of T st for A being Subset of T st A in
BB & inf F in A holds F meets A holds inf F in Cl F
proof
let T be lower complete TopLattice, BB be prebasis of T;
let F be non empty filtered Subset of T such that
A1: for A being Subset of T st A in BB & inf F in A holds F meets A;
set N = F opp+id, x = inf F;
A2: for A being Subset of T st A in BB & x in A holds N is_eventually_in A
proof
let A be Subset of T;
assume that
A3: A in BB and
A4: x in A;
A is open by A3,TOPS_2:def 1;
then
A5: A is lower by Th5;
F meets A by A3,A4,A1;
then consider i being object such that
A6: i in F and
A7: i in A by XBOOLE_0:3;
reconsider i as Element of N by A6,YELLOW_9:7;
take i;
let j be Element of N;
A8: N is full SubRelStr of T opp by YELLOW_9:7;
then reconsider a = i, b = j as Element of T opp by YELLOW_0:58;
assume i <= j;
then a <= b by A8,YELLOW_0:59;
then
A9: ~b <= ~a by YELLOW_7:1;
N.j = j by YELLOW_9:7;
hence thesis by A9,A7,A5;
end;
A10: the carrier of N = F by YELLOW_9:7;
rng netmap(N,T) c= F
proof
let x be object;
assume x in rng netmap(N,T);
then consider a being object such that
A11: a in dom netmap(N,T) and
A12: x = (netmap(N,T)).a by FUNCT_1:def 3;
reconsider a as Element of N by A11;
x = N.a by A12
.= a by YELLOW_9:7;
hence thesis by A10;
end;
hence thesis by A2,YELLOW_9:39;
end;
theorem Th11:
:: 1.2. LEMMA (ii), p. 143
for S,T being lower complete TopLattice for f being Function of
S,T st f is continuous holds f is filtered-infs-preserving
proof
let S,T be lower complete TopLattice;
reconsider BB = the set of all (uparrow x)` where x is Element of S as
prebasis of S by Def1;
let f be Function of S,T such that
A1: f is continuous;
let F be Subset of S such that
A2: F is non empty filtered and
ex_inf_of F,S;
for A being Subset of S st A in BB & inf F in A holds F meets A
proof
let A be Subset of S;
assume A in BB;
then consider x being Element of S such that
A3: A = (uparrow x)`;
assume inf F in A;
then not inf F >= x by A3,YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of S such that
A4: y in F and
A5: not y >= x;
y in A by A3,A5,YELLOW_9:1;
hence thesis by A4,XBOOLE_0:3;
end;
then
A6: inf F in Cl F by A2,Th10;
A7: f is monotone
proof
let x,y be Element of S such that
A8: x <= y;
f.x <= f.x;
then f.x in uparrow (f.x) by WAYBEL_0:18;
then
A9: x in f"uparrow (f.x) by FUNCT_2:38;
uparrow (f.x) is closed by Th4;
then f"uparrow (f.x) is closed by A1;
then f"uparrow (f.x) is upper by Th6;
then y in f"uparrow (f.x) by A9,A8;
then f.y in uparrow (f.x) by FUNCT_2:38;
hence thesis by WAYBEL_0:18;
end;
f.inf F is_<=_than f.:F
proof
let x be Element of T;
assume x in f.:F;
then consider a being object such that
A10: a in the carrier of S and
A11: a in F and
A12: x = f.a by FUNCT_2:64;
reconsider a as Element of S by A10;
inf F is_<=_than F by YELLOW_0:33;
then inf F <= a by A11;
hence thesis by A7,A12;
end;
then
A13: f.inf F <= inf (f.:F) by YELLOW_0:33;
thus ex_inf_of f.:F,T by YELLOW_0:17;
F c= f"uparrow inf (f.:F)
proof
let x be object;
assume
A14: x in F;
then reconsider s = x as Element of S;
f.s in f.:F by A14,FUNCT_2:35;
then inf (f.:F) <= f.s by YELLOW_2:22;
then f.s in uparrow inf (f.:F) by WAYBEL_0:18;
hence thesis by FUNCT_2:38;
end;
then
A15: Cl F c= Cl (f"uparrow inf (f.:F)) by PRE_TOPC:19;
uparrow inf (f.:F) is closed by Th4;
then f"uparrow inf (f.:F) is closed by A1;
then Cl F c= f"uparrow inf (f.:F) by A15,PRE_TOPC:22;
then f.inf F in uparrow inf (f.:F) by A6,FUNCT_2:38;
then f.inf F >= inf (f.:F) by WAYBEL_0:18;
hence inf (f.:F) = f.inf F by A13,ORDERS_2:2;
end;
theorem
:: 1.2. LEMMA (iii), p. 143
for S,T being lower complete TopLattice for f being Function of S,T st
f is continuous & for X being finite Subset of S holds f preserves_inf_of X
holds f is infs-preserving
proof
let S,T be lower complete TopLattice;
let f be Function of S,T;
assume f is continuous;
then f is filtered-infs-preserving by Th11;
then
for F being filtered non empty Subset of S holds f preserves_inf_of F;
hence thesis by WAYBEL_0:71;
end;
theorem
:: Remark before 1.3., p. 143
for T being lower TopSpace-like reflexive transitive non empty
TopRelStr for x being Point of T holds Cl {x} = uparrow x
proof
let T be lower TopSpace-like reflexive transitive non empty TopRelStr;
let x be Point of T;
reconsider y = x as Element of T;
y <= y;
then x in uparrow x by WAYBEL_0:18;
then {x} c= uparrow x by ZFMISC_1:31;
hence Cl {x} c= uparrow x by Th4,TOPS_1:5;
Cl {x} is upper by Th6;
then
A1: uparrow Cl {x} c= Cl {x} by WAYBEL_0:24;
uparrow {x} c= uparrow Cl {x} by PRE_TOPC:18,YELLOW_3:7;
hence thesis by A1;
end;
definition
mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr;
end;
registration
:: Remark before 1.3., p. 143
cluster lower -> T_0 for non empty TopPoset;
coherence
proof
let T be non empty TopPoset such that
A1: T is lower;
now
assume T is not empty;
let x,y be Point of T such that
A2: x <> y;
reconsider a = x, b = y as Element of T;
set Vy = (uparrow a)`, Vx = (uparrow b)`;
a <= a;
then
A3: not x in Vy by YELLOW_9:1;
b <= b;
then
A4: not y in Vx by YELLOW_9:1;
A5: Vx is open by A1,Th4;
A6: Vy is open by A1,Th4;
per cases by A2,YELLOW_0:def 3;
suppose
not b <= a;
then a in Vx by YELLOW_9:1;
hence
(ex V being Subset of T st V is open & x in V & not y in V) or ex
V being Subset of T st V is open & not x in V & y in V by A5,A4;
end;
suppose
not a <= b;
then b in Vy by YELLOW_9:1;
hence
(ex V being Subset of T st V is open & x in V & not y in V) or ex
V being Subset of T st V is open & not x in V & y in V by A6,A3;
end;
end;
hence thesis by TSP_1:def 3;
end;
end;
registration
let R be lower-bounded non empty RelStr;
cluster -> lower-bounded for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of R = the RelStr of T by YELLOW_9:def 4;
hence thesis by YELLOW_0:13;
end;
end;
theorem Th14:
for S, T being non empty RelStr, s being Element of S, t being
Element of T holds (uparrow [s,t])` = [:(uparrow s)`, the carrier of T:] \/ [:
the carrier of S, (uparrow t)`:]
proof
let S, T be non empty RelStr, s be Element of S, t be Element of T;
thus (uparrow [s,t])` = [:the carrier of S, the carrier of T:] \ uparrow [s,
t] by YELLOW_3:def 2
.= [:the carrier of S, the carrier of T:] \ [:uparrow s, uparrow t:] by
YELLOW10:40
.= [:(uparrow s)`, the carrier of T:] \/ [:the carrier of S, (uparrow t)
`:] by ZFMISC_1:103;
end;
theorem Th15:
:: 1.3. LEMMA, p. 143 (variant I)
for S,T being lower-bounded non empty Poset for S9 being lower
correct TopAugmentation of S for T9 being lower correct TopAugmentation of T
holds omega [:S,T:] = the topology of [:S9,T9 qua non empty TopSpace:]
proof
let S,T be lower-bounded non empty Poset;
set ST = the lower correct TopAugmentation of [:S,T:];
reconsider BX = the set of all (uparrow x)` where x is Element of ST
as prebasis of ST by Def1;
let S9 be lower correct TopAugmentation of S;
reconsider BS = the set of all (uparrow x)` where x is Element of S9
as prebasis of S9 by Def1;
let T9 be lower correct TopAugmentation of T;
set SxT = [:S9,T9 qua non empty TopSpace:];
set B2 = {[:a, the carrier of T9:] where a is Subset of S9: a in BS};
A1: the RelStr of T9 = the RelStr of T by YELLOW_9:def 4;
reconsider BT = the set of all (uparrow x)` where x is Element of T9
as prebasis of T9 by Def1;
A2: the RelStr of S9 = the RelStr of S by YELLOW_9:def 4;
then
A3: the carrier of SxT = [:the carrier of S, the carrier of T:] by A1,
BORSUK_1:def 2;
A4: the RelStr of ST = [:S,T:] by YELLOW_9:def 4;
then
A5: the carrier of ST = [:the carrier of S, the carrier of T:] by
YELLOW_3:def 2;
A6: BX c= the topology of SxT
proof
let z be object;
A7: [#] T9 is open;
assume z in BX;
then consider x being Element of ST such that
A8: z = (uparrow x)`;
consider s,t being object such that
A9: s in the carrier of S and
A10: t in the carrier of T and
A11: x = [s,t] by A5,ZFMISC_1:def 2;
reconsider t as Element of T by A10;
reconsider s as Element of S by A9;
uparrow x = uparrow [s,t] by A4,A11,WAYBEL_0:13;
then
A12: z = [:(uparrow s)`, [#]T:] \/ [:[#]S, (uparrow t)`:] by A4,A8,Th14;
reconsider s9 = s as Element of S9 by A2;
reconsider t9 = t as Element of T9 by A1;
(uparrow t9)` in BT;
then
A13: (uparrow t9)` is open by TOPS_2:def 1;
reconsider A1 = [:(uparrow s)`, [#]T:], A2 = [:[#]S, (uparrow t)`:] as
Subset of SxT by A3,YELLOW_3:def 2;
A14: [#]S9 is open;
(uparrow s9)` in BS;
then
A15: (uparrow s9)` is open by TOPS_2:def 1;
uparrow t = uparrow t9 by A1,WAYBEL_0:13;
then
A16: A2 is open by A13,A14,A2,A1,BORSUK_1:6;
uparrow s = uparrow s9 by A2,WAYBEL_0:13;
then A1 is open by A15,A7,A2,A1,BORSUK_1:6;
then A1 \/ A2 is open by A16;
hence thesis by A12;
end;
set B1 = {[:the carrier of S9, b:] where b is Subset of T9: b in BT};
reconsider BB = B1 \/ B2 as prebasis of SxT by YELLOW_9:41;
A17: UniCl the topology of SxT = the topology of SxT by CANTOR_1:6;
BB c= BX
proof
let z be object;
assume
A18: z in BB;
per cases by A18,XBOOLE_0:def 3;
suppose
z in B1;
then consider b being Subset of T9 such that
A19: z = [:the carrier of S9, b:] and
A20: b in BT;
consider t9 being Element of T9 such that
A21: b = (uparrow t9)` by A20;
reconsider t = t9 as Element of T by A1;
reconsider x = [Bottom S,t] as Element of ST by A4;
A22: uparrow x = uparrow [Bottom S,t] by A4,WAYBEL_0:13;
uparrow Bottom S = the carrier of S by WAYBEL14:10;
then
A23: (uparrow Bottom S)` = {} by XBOOLE_1:37;
uparrow t = uparrow t9 by A1,WAYBEL_0:13;
then
(uparrow [Bottom S,t])` = [:{}, the carrier of T:] \/ [:the carrier
of S, b:] by A23,A1,A21,Th14
.= {} \/ [:the carrier of S, b:] by ZFMISC_1:90
.= z by A2,A19;
hence thesis by A4,A22;
end;
suppose
z in B2;
then consider a being Subset of S9 such that
A24: z = [:a, the carrier of T9:] and
A25: a in BS;
consider s9 being Element of S9 such that
A26: a = (uparrow s9)` by A25;
reconsider s = s9 as Element of S by A2;
reconsider x = [s,Bottom T] as Element of ST by A4;
A27: uparrow x = uparrow [s,Bottom T] by A4,WAYBEL_0:13;
uparrow Bottom T = the carrier of T by WAYBEL14:10;
then
A28: (uparrow Bottom T)` = {} by XBOOLE_1:37;
uparrow s = uparrow s9 by A2,WAYBEL_0:13;
then (uparrow [s,Bottom T])` = [:a, the carrier of T:] \/ [:the carrier
of S, {}:] by A28,A2,A26,Th14
.= [:a, the carrier of T:] \/ {} by ZFMISC_1:90
.= z by A1,A24;
hence thesis by A4,A27;
end;
end;
then FinMeetCl BB c= FinMeetCl BX by A5,A3,CANTOR_1:14;
then
A29: UniCl FinMeetCl BB c= UniCl FinMeetCl BX by A5,A3,CANTOR_1:9;
FinMeetCl BB is Basis of SxT by YELLOW_9:23;
then
A30: the topology of SxT = UniCl FinMeetCl BB by YELLOW_9:22;
FinMeetCl BX is Basis of ST by YELLOW_9:23;
then
A31: the topology of ST = UniCl FinMeetCl BX by YELLOW_9:22;
FinMeetCl the topology of SxT = the topology of SxT by CANTOR_1:5;
then FinMeetCl BX c= the topology of SxT by A6,A5,A3,CANTOR_1:14;
then UniCl FinMeetCl BX c= the topology of SxT by A5,A3,A17,CANTOR_1:9;
then the topology of ST = the topology of SxT by A31,A30,A29;
hence thesis by Def2;
end;
theorem
:: 1.3. LEMMA, p. 143 (variant II)
for S,T being lower lower-bounded non empty TopPoset holds omega [:S
,T qua Poset:] = the topology of [:S,T qua non empty TopSpace:]
proof
let S,T be lower lower-bounded non empty TopPoset;
A1: T is TopAugmentation of T by YELLOW_9:44;
S is TopAugmentation of S by YELLOW_9:44;
hence thesis by A1,Th15;
end;
theorem
:: 1.4. LEMMA, p. 144:: Refinements
for T,T2 being lower complete TopLattice st T2 is TopAugmentation of
[:T, T qua LATTICE:] for f being Function of T2,T st f = inf_op T holds f is
continuous
proof
let T,T2 be lower complete TopLattice such that
A1: the RelStr of T2 = the RelStr of [:T, T:];
let f be Function of T2,T such that
A2: f = inf_op T;
f is infs-preserving
proof
let X be Subset of T2;
reconsider Y = X as Subset of [:T,T:] by A1;
assume
A3: ex_inf_of X,T2;
thus ex_inf_of f.:X,T by YELLOW_0:17;
A4: inf_op T preserves_inf_of Y by WAYBEL_0:def 32;
ex_inf_of Y, [:T,T:] by A3,A1,YELLOW_0:14;
hence inf (f.:X) = f.inf X by A1,A2,A4,YELLOW_0:27;
end;
hence thesis by Th9;
end;
begin :: Refinements
scheme
TopInd {T() -> TopLattice, P[set]}: for A being Subset of T() st A is open
holds P[A]
provided
A1: ex K being prebasis of T() st for A being Subset of T() st A in K
holds P[A] and
A2: for F being Subset-Family of T() st for A being Subset of T() st A
in F holds P[A] holds P[union F] and
A3: for A1,A2 being Subset of T() st P[A1] & P[A2] holds P[A1 /\ A2] and
A4: P[[#]T()]
proof
consider K being prebasis of T() such that
A5: for A being Subset of T() st A in K holds P[A] by A1;
let A be Subset of T();
assume
A6: A in the topology of T();
FinMeetCl K is Basis of T() by YELLOW_9:23;
then UniCl FinMeetCl K = the topology of T() by YELLOW_9:22;
then consider X being Subset-Family of T() such that
A7: X c= FinMeetCl K and
A8: A = union X by A6,CANTOR_1:def 1;
reconsider X as Subset-Family of T();
now
defpred Q[set] means for a being Subset-Family of T() st a = $1 holds P[
Intersect a];
let A be Subset of T();
assume A in X;
then consider Y being Subset-Family of T() such that
A9: Y c= K and
A10: Y is finite and
A11: A = Intersect Y by A7,CANTOR_1:def 3;
A12: for x,Z being set st x in Y & Z c= Y & Q[Z] holds Q[Z \/ {x}]
proof
let x,Z be set;
assume that
A13: x in Y and
A14: Z c= Y and
A15: Q[Z];
reconsider xx = {x}, Z9 = Z as Subset-Family of T() by A13,A14,XBOOLE_1:1
,ZFMISC_1:31;
reconsider xx, Z9 as Subset-Family of T();
reconsider xx, Z9 as Subset-Family of T();
reconsider Ax = x, Ay = Intersect Z9 as Subset of T() by A13;
A16: P[Ay] by A15;
let a be Subset-Family of T();
assume
A17: a = Z \/ {x};
Intersect xx = Ax by MSSUBFAM:9;
then
A18: Intersect a = Ax /\ Ay by A17,MSSUBFAM:8;
P[Ax] by A5,A9,A13;
hence thesis by A18,A3,A16;
end;
A19: Q[{}] by A4,SETFAM_1:def 9;
Q[Y] from FINSET_1:sch 2(A10,A19,A12);
hence P[A] by A11;
end;
hence thesis by A2,A8;
end;
theorem
for L1,L2 being up-complete antisymmetric non empty reflexive RelStr
st the RelStr of L1 = the RelStr of L2 & for x being Element of L1 holds
waybelow x is directed non empty holds L1 is satisfying_axiom_of_approximation
implies L2 is satisfying_axiom_of_approximation
proof
let L1,L2 be up-complete antisymmetric non empty reflexive RelStr such
that
A1: the RelStr of L1 = the RelStr of L2 and
A2: for x being Element of L1 holds waybelow x is directed non empty and
A3: for x being Element of L1 holds x = sup waybelow x;
let x be Element of L2;
reconsider y = x as Element of L1 by A1;
A4: y = sup waybelow y by A3;
waybelow y is directed non empty by A2;
then
A5: ex_sup_of waybelow y, L1 by WAYBEL_0:75;
waybelow y = waybelow x by A1,YELLOW12:13;
hence thesis by A4,A5,A1,YELLOW_0:26;
end;
registration
let T be continuous non empty Poset;
cluster -> continuous for TopAugmentation of T;
coherence
proof
let S be TopAugmentation of T;
the RelStr of S = the RelStr of T by YELLOW_9:def 4;
hence thesis by YELLOW12:15;
end;
end;
theorem Th19:
for T,S being TopSpace, R being Refinement of T,S for W being
Subset of R st W in the topology of T or W in the topology of S holds W is open
proof
let T,S be TopSpace, R be Refinement of T,S;
let W be Subset of R;
(the topology of T) \/ the topology of S is prebasis of R by YELLOW_9:def 6;
then
A1: (the topology of T) \/ the topology of S c= the topology of R by TOPS_2:64;
assume W in the topology of T or W in the topology of S;
then W in (the topology of T) \/ the topology of S by XBOOLE_0:def 3;
hence W in the topology of R by A1;
end;
theorem Th20:
for T,S being TopSpace, R being Refinement of T,S for V being
Subset of T, W being Subset of R st W = V holds V is open implies W is open
by Th19;
theorem Th21:
for T,S being TopSpace st the carrier of T = the carrier of S
for R being Refinement of T,S for V being Subset of T, W being Subset of R st W
= V holds V is closed implies W is closed
proof
let T,S be TopSpace such that
A1: the carrier of T = the carrier of S;
let R be Refinement of T,S;
let V be Subset of T, W be Subset of R;
assume
A2: W = V;
assume V is closed;
then
A3: V` is open;
the carrier of R = (the carrier of T) \/ the carrier of S by YELLOW_9:def 6
.= the carrier of T by A1;
then W` in the topology of T by A3,A2;
then W` is open by Th19;
hence thesis;
end;
theorem Th22:
for T being non empty TopSpace, K,O being set st K c= O & O c=
the topology of T holds (K is Basis of T implies O is Basis of T) & (K is
prebasis of T implies O is prebasis of T)
proof
let T be non empty TopSpace, K,O be set;
assume that
A1: K c= O and
A2: O c= the topology of T;
K c= the topology of T by A1,A2;
then reconsider K9 = K, O9 = O as Subset-Family of T by A2,XBOOLE_1:1;
reconsider K9, O9 as Subset-Family of T;
reconsider K9, O9 as Subset-Family of T;
A3: UniCl K9 c= UniCl O9 by A1,CANTOR_1:9;
A4: UniCl the topology of T = the topology of T by CANTOR_1:6;
then
A5: UniCl O9 c= the topology of T by A2,CANTOR_1:9;
hereby
assume K is Basis of T;
then UniCl K9 = the topology of T by YELLOW_9:22;
then UniCl O9 = the topology of T by A5,A3;
hence O is Basis of T by YELLOW_9:22;
end;
FinMeetCl the topology of T = the topology of T by CANTOR_1:5;
then FinMeetCl O9 c= the topology of T by A2,CANTOR_1:14;
then
A6: UniCl FinMeetCl O9 c= the topology of T by A4,CANTOR_1:9;
assume K is prebasis of T;
then FinMeetCl K9 is Basis of T by YELLOW_9:23;
then
A7: UniCl FinMeetCl K9 = the topology of T by YELLOW_9:22;
FinMeetCl K9 c= FinMeetCl O9 by A1,CANTOR_1:14;
then UniCl FinMeetCl K9 c= UniCl FinMeetCl O9 by CANTOR_1:9;
then UniCl FinMeetCl O9 = the topology of T by A7,A6;
then FinMeetCl O9 is Basis of T by YELLOW_9:22;
hence thesis by YELLOW_9:23;
end;
theorem Th23:
:: YELLOW_9:58 revised
for T1,T2 being non empty TopSpace st the carrier of T1 = the
carrier of T2 for T be Refinement of T1, T2 for B1 being prebasis of T1, B2
being prebasis of T2 holds B1 \/ B2 is prebasis of T
proof
let T1,T2 be non empty TopSpace such that
A1: the carrier of T1 = the carrier of T2;
let T be Refinement of T1, T2;
let B1 be prebasis of T1, B2 be prebasis of T2;
the carrier of T = (the carrier of T1) \/ the carrier of T2 by YELLOW_9:def 6
.= the carrier of T1 by A1;
then {the carrier of T1, the carrier of T2} = {the carrier of T} by A1,
ENUMSET1:29;
then reconsider K = B1 \/ B2 \/ {the carrier of T} as prebasis of T by
YELLOW_9:58;
B1 \/ B2 c= K by XBOOLE_1:7;
then reconsider K9 = B1 \/ B2 as Subset-Family of T by XBOOLE_1:1;
K c= FinMeetCl K9
proof
let a be object;
assume a in K;
then
a in K9 & K9 c= FinMeetCl K9 or a in {the carrier of T} & the carrier
of T in FinMeetCl K9 by CANTOR_1:4,8,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
then FinMeetCl K c= FinMeetCl FinMeetCl K9 by CANTOR_1:14;
then
A2: FinMeetCl K c= FinMeetCl K9 by CANTOR_1:11;
FinMeetCl K9 c= FinMeetCl K by CANTOR_1:14,XBOOLE_1:7;
then FinMeetCl K9 = FinMeetCl K by A2;
then FinMeetCl K9 is Basis of T by YELLOW_9:23;
hence thesis by YELLOW_9:23;
end;
theorem
for T1,S1,T2,S2 being non empty TopSpace for R1 being Refinement of T1
,S1, R2 being Refinement of T2,S2 for f being Function of T1,T2, g being
Function of S1,S2 for h being Function of R1,R2 st h = f & h = g holds f is
continuous & g is continuous implies h is continuous
proof
let T1,S1,T2,S2 be non empty TopSpace;
let R1 be Refinement of T1,S1, R2 be Refinement of T2,S2;
let f be Function of T1,T2, g be Function of S1,S2;
let h be Function of R1,R2 such that
A1: h = f and
A2: h = g;
A3: [#]S2 <> {};
reconsider K = (the topology of T2) \/ the topology of S2 as prebasis of R2
by YELLOW_9:def 6;
A4: [#]T2 <> {};
assume
A5: f is continuous;
assume
A6: g is continuous;
now
let A be Subset of R2;
assume
A7: A in K;
per cases by A7,XBOOLE_0:def 3;
suppose
A8: A in the topology of T2;
then reconsider A1 = A as Subset of T2;
A1 is open by A8;
then f"A1 is open by A4,A5,TOPS_2:43;
hence h"A is open by A1,Th20;
end;
suppose
A9: A in the topology of S2;
then reconsider A1 = A as Subset of S2;
A1 is open by A9;
then
A10: g"A1 is open by A3,A6,TOPS_2:43;
R1 is Refinement of S1,T1 by YELLOW_9:55;
hence h"A is open by A10,A2,Th20;
end;
end;
hence thesis by YELLOW_9:36;
end;
theorem Th25:
for T being non empty TopSpace, K being prebasis of T for N
being net of T, p being Point of T st for A being Subset of T st p in A & A in
K holds N is_eventually_in A holds p in Lim N
proof
let T be non empty TopSpace, K be prebasis of T;
let N be net of T, x be Point of T such that
A1: for A being Subset of T st x in A & A in K holds N is_eventually_in A;
now
defpred P[object,object] means
ex D1 being set st D1 = $1 &
for i,j being Element of N st i = $2 & j >= i
holds N.j in D1;
let A be a_neighborhood of x;
A2: Int A in the topology of T by PRE_TOPC:def 2;
FinMeetCl K is Basis of T by YELLOW_9:23;
then the topology of T = UniCl FinMeetCl K by YELLOW_9:22;
then consider Y being Subset-Family of T such that
A3: Y c= FinMeetCl K and
A4: Int A = union Y by A2,CANTOR_1:def 1;
x in Int A by CONNSP_2:def 1;
then consider y being set such that
A5: x in y and
A6: y in Y by A4,TARSKI:def 4;
consider Z being Subset-Family of T such that
A7: Z c= K and
A8: Z is finite and
A9: y = Intersect Z by A3,A6,CANTOR_1:def 3;
A10: for a being object st a in Z
ex b being object st b in the carrier of N & P[a,b]
proof
let a be object;
assume
A11: a in Z;
then reconsider a as Subset of T;
x in a by A5,A9,A11,SETFAM_1:43;
then N is_eventually_in a by A1,A7,A11;
then consider i being Element of N such that
A12: for j being Element of N st j >= i holds N.j in a;
reconsider i as object;
take i;
thus i in the carrier of N;
take a;
thus thesis by A12;
end;
consider f being Function such that
A13: dom f = Z & rng f c= the carrier of N and
A14: for a being object st a in Z holds P[a,f.a] from FUNCT_1:sch 6(A10);
reconsider z = rng f as finite Subset of [#]N by A8,A13,FINSET_1:8;
[#]N is directed by WAYBEL_0:def 6;
then consider k being Element of N such that
k in [#]N and
A15: k is_>=_than z by WAYBEL_0:1;
thus N is_eventually_in A
proof
take k;
let i be Element of N;
A16: Int A c= A by TOPS_1:16;
assume
A17: i >= k;
now
let a be set;
assume
A18: a in Z;
then
A19: f.a in z by A13,FUNCT_1:def 3;
then reconsider j = f.a as Element of N;
A20: j <= k by A15,A19;
P[a,f.a] by A14,A18;
then consider D1 being set such that
A21: D1 = a &
for i,j being Element of N st i = f.a & j >= i
holds N.j in D1;
thus N.i in a by A17,ORDERS_2:3,A21,A20;
end;
then
A22: N.i in y by A9,SETFAM_1:43;
y c= union Y by A6,ZFMISC_1:74;
then N.i in Int A by A22,A4;
hence thesis by A16;
end;
end;
hence thesis by YELLOW_6:def 15;
end;
theorem Th26:
for T being non empty TopSpace for N being net of T for S being
Subset of T st N is_eventually_in S holds Lim N c= Cl S
proof
let T be non empty TopSpace, N be net of T, S be Subset of T;
given i being Element of N such that
A1: for j being Element of N st j >= i holds N.j in S;
let x be object;
assume
A2: x in Lim N;
then reconsider x as Element of T;
now
let G be a_neighborhood of x;
N is_eventually_in G by A2,YELLOW_6:def 15;
then consider k being Element of N such that
A3: for j being Element of N st j >= k holds N.j in G;
[#]N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#]N and
A4: j >= i and
A5: j >= k;
A6: N.j in G by A3,A5;
N.j in S by A1,A4;
hence G meets S by A6,XBOOLE_0:3;
end;
hence thesis by CONNSP_2:27;
end;
theorem Th27:
for R being non empty RelStr, X being non empty Subset of R
holds the mapping of X+id = id X & the mapping of X opp+id = id X
proof
let R be non empty RelStr, X be non empty Subset of R;
A1: now
let x be object;
assume x in X;
then reconsider i = x as Element of X+id by YELLOW_9:6;
thus (the mapping of X+id).x = X+id.i .= x by YELLOW_9:6;
end;
the carrier of X+id = X by YELLOW_9:6;
then dom the mapping of X+id = X by FUNCT_2:def 1;
hence the mapping of X+id = id X by A1,FUNCT_1:17;
A2: now
let x be object;
assume x in X;
then reconsider i = x as Element of X opp+id by YELLOW_9:7;
thus (the mapping of X opp+id).x = X opp+id.i .= x by YELLOW_9:7;
end;
the carrier of X opp+id = X by YELLOW_9:7;
then dom the mapping of X opp+id = X by FUNCT_2:def 1;
hence thesis by A2,FUNCT_1:17;
end;
theorem Th28:
for R being reflexive antisymmetric non empty RelStr, x being
Element of R holds (uparrow x) /\ (downarrow x) = {x}
proof
let R be reflexive antisymmetric non empty RelStr, x be Element of R;
hereby
let a be object;
assume
A1: a in (uparrow x) /\ (downarrow x);
then reconsider y = a as Element of R;
y in downarrow x by A1,XBOOLE_0:def 4;
then
A2: y <= x by WAYBEL_0:17;
y in uparrow x by A1,XBOOLE_0:def 4;
then x <= y by WAYBEL_0:18;
then x = a by A2,ORDERS_2:2;
hence a in {x} by TARSKI:def 1;
end;
A3: x <= x;
then
A4: x in downarrow x by WAYBEL_0:17;
x in uparrow x by A3,WAYBEL_0:18;
then x in (uparrow x) /\ (downarrow x) by A4,XBOOLE_0:def 4;
hence thesis by ZFMISC_1:31;
end;
begin :: Lawson topology
definition
let T be reflexive non empty TopRelStr;
attr T is Lawson means
: Def3:
(omega T) \/ (sigma T) is prebasis of T;
end;
theorem Th29:
for R being complete LATTICE for LL being lower correct
TopAugmentation of R for S being Scott TopAugmentation of R for T being correct
TopAugmentation of R holds T is Lawson iff T is Refinement of S,LL
proof
let R be complete LATTICE;
let LL be lower correct TopAugmentation of R;
let S be Scott TopAugmentation of R;
let T be correct TopAugmentation of R;
A1: the topology of S = sigma R by YELLOW_9:51;
A2: (the carrier of R) \/ the carrier of R = the carrier of R;
A3: the topology of LL = omega R by Def2;
A4: the RelStr of LL = the RelStr of R by YELLOW_9:def 4;
A5: the RelStr of S = the RelStr of R by YELLOW_9:def 4;
A6: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
then
A7: sigma T = sigma R by YELLOW_9:52;
omega T = omega R by A6,Th3;
hence thesis by A7,A3,A1,A2,A4,A5,A6,YELLOW_9:def 6;
end;
registration
let R be complete LATTICE;
cluster Lawson strict correct for TopAugmentation of R;
existence
proof
set S = the Scott correct TopAugmentation of R;
set T = the lower correct TopAugmentation of R;
A1: the RelStr of S = the RelStr of R by YELLOW_9:def 4;
set RR = the Refinement of S,T;
A2: the carrier of RR = (the carrier of S) \/ the carrier of T by
YELLOW_9:def 6;
A3: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
then reconsider O = the topology of RR as Subset-Family of R by A2,A1;
set LL = TopRelStr(#the carrier of R, the InternalRel of R, O#);
the RelStr of LL = the RelStr of R;
then reconsider LL as TopAugmentation of R by YELLOW_9:def 4;
the TopStruct of LL = the TopStruct of RR by A3,A1,A2;
then
A4: LL is correct by TEX_2:7;
reconsider A = (the topology of S) \/ (the topology of T) as prebasis of
RR by YELLOW_9:def 6;
reconsider A9 = A as Subset-Family of LL by A3,A1,A2;
take LL;
FinMeetCl A is Basis of RR by YELLOW_9:23;
then UniCl FinMeetCl A = O by YELLOW_9:22;
then FinMeetCl A9 is Basis of LL by A3,A1,A2,A4,YELLOW_9:22;
then (the topology of S) \/ (the topology of T) is prebasis of LL by A4,
YELLOW_9:23;
then LL is Refinement of S,T by A3,A1,A2,A4,YELLOW_9:def 6;
hence thesis by Th29;
end;
end;
registration
cluster Scott complete strict for TopLattice;
existence
proof
set R = the complete LATTICE;
set T = the strict Scott correct TopAugmentation of R;
take T;
thus thesis;
end;
cluster Lawson continuous for complete strict TopLattice;
existence
proof
set R = the continuous complete LATTICE;
set T = the strict Lawson correct TopAugmentation of R;
take T;
thus thesis;
end;
end;
theorem Th30:
for T being Lawson complete TopLattice holds (sigma T) \/ the set of all (
uparrow x)` where x is Element of T is prebasis of T
proof
let T be Lawson complete TopLattice;
set R = the lower correct TopAugmentation of T;
set S = the Scott TopAugmentation of T;
A1: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
T is TopAugmentation of T by YELLOW_9:44;
then
A2: T is Refinement of S,R by Th29;
set K = the set of all (uparrow x)` where x is Element of R;
set O = the set of all (uparrow x)` where x is Element of T;
the topology of S = sigma T by YELLOW_9:51;
then sigma T is Basis of S by CANTOR_1:2;
then
A3: sigma T is prebasis of S by YELLOW_9:27;
A4: the RelStr of R = the RelStr of T by YELLOW_9:def 4;
O = K
proof
hereby
let a be object;
assume a in O;
then consider x being Element of T such that
A5: a = (uparrow x)`;
reconsider y = x as Element of R by A4;
uparrow x = uparrow y by A4,WAYBEL_0:13;
hence a in K by A4,A5;
end;
let a be object;
assume a in K;
then consider x being Element of R such that
A6: a = (uparrow x)`;
reconsider y = x as Element of T by A4;
uparrow x = uparrow y by A4,WAYBEL_0:13;
hence thesis by A4,A6;
end;
then reconsider O as prebasis of R by Def1;
O = O;
hence thesis by A3,A2,A1,A4,Th23;
end;
theorem
for T being Lawson complete TopLattice holds (sigma T) \/ {W\uparrow
x where W is Subset of T, x is Element of T: W in sigma T} is prebasis of T
proof
let T be Lawson complete TopLattice;
set R = the lower correct TopAugmentation of T;
reconsider K = the set of all (uparrow x)` where x is Element of R as
prebasis of R by Def1;
set O = {W\uparrow x where W is Subset of T,x is Element of T: W in sigma T};
O c= bool the carrier of T
proof
let a be object;
assume a in O;
then
ex W being Subset of T, x being Element of T st a = W\uparrow x & W in
sigma T;
hence thesis;
end;
then reconsider O as Subset-Family of T;
reconsider O as Subset-Family of T;
set S = the Scott TopAugmentation of T;
A1: the RelStr of R = the RelStr of T by YELLOW_9:def 4;
(sigma T) \/ omega T is prebasis of T by Def3;
then
A2: (sigma T) \/ omega T c= the topology of T by TOPS_2:64;
omega T c= (sigma T) \/ omega T by XBOOLE_1:7;
then
A3: omega T c= the topology of T by A2;
sigma T c= (sigma T) \/ omega T by XBOOLE_1:7;
then
A4: sigma T c= the topology of T by A2;
A5: omega T = the topology of R by Def2;
O c= the topology of T
proof
let a be object;
assume a in O;
then consider W being Subset of T, x being Element of T such that
A6: a = W \ uparrow x and
A7: W in sigma T;
A8: a = W /\ (uparrow x)` by A6,SUBSET_1:13;
reconsider y = x as Element of R by A1;
uparrow x = uparrow y by A1,WAYBEL_0:13;
then
A9: (uparrow x)` in K by A1;
K c= omega T by A5,TOPS_2:64;
then (uparrow x)` in omega T by A9;
hence thesis by A4,A3,A7,A8,PRE_TOPC:def 1;
end;
then
A10: (sigma T) \/ O c= the topology of T by A4,XBOOLE_1:8;
A11: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
A12: sigma T = the topology of S by YELLOW_9:51;
then sigma T is Basis of S by CANTOR_1:2;
then
A13: sigma T is prebasis of S by YELLOW_9:27;
A14: the carrier of S in sigma T by A12,PRE_TOPC:def 1;
K c= O
proof
let a be object;
assume a in K;
then consider x being Element of R such that
A15: a = (uparrow x)`;
reconsider y = x as Element of T by A1;
a = [#]T\uparrow y by A1,A15,WAYBEL_0:13;
hence thesis by A11,A14;
end;
then
A16: (sigma T) \/ K c= (sigma T) \/ O by XBOOLE_1:9;
T is TopAugmentation of T by YELLOW_9:44;
then T is Refinement of S,R by Th29;
hence thesis by A13,A1,A11,Th23,A16,A10,Th22;
end;
theorem
for T being Lawson complete TopLattice holds {W\uparrow F where W,F
is Subset of T: W in sigma T & F is finite} is Basis of T
proof
let T be Lawson complete TopLattice;
set R = the lower correct TopAugmentation of T;
reconsider B2 = {(uparrow F)` where F is Subset of R: F is finite} as Basis
of R by Th7;
set Z = {W\uparrow F where W,F is Subset of T: W in sigma T & F is finite};
set S = the Scott TopAugmentation of T;
A1: the topology of S = sigma T by YELLOW_9:51;
then reconsider B1 = sigma T as Basis of S by CANTOR_1:2;
A2: the RelStr of R = the RelStr of T by YELLOW_9:def 4;
B1 c= Z
proof
set F9 = {}R;
reconsider G = F9 as Subset of T by A2;
let x be object;
assume
A3: x in B1;
then reconsider x9 = x as Subset of T;
uparrow G = uparrow F9;
then x9\uparrow G = x9;
hence thesis by A3;
end;
then
A4: B1 \/ Z = Z by XBOOLE_1:12;
A5: INTERSECTION(B1,B2) = Z
proof
hereby
let x be object;
assume x in INTERSECTION(B1,B2);
then consider y,z being set such that
A6: y in B1 and
A7: z in B2 and
A8: x = y /\ z by SETFAM_1:def 5;
reconsider y as Subset of T by A6;
A9: [#]T /\ y = y by XBOOLE_1:28;
consider F being Subset of R such that
A10: z = (uparrow F)` and
A11: F is finite by A7;
reconsider G = F as Subset of T by A2;
z = (uparrow G)` by A2,A10,WAYBEL_0:13;
then x = y\uparrow G by A9,A8,XBOOLE_1:49;
hence x in Z by A6,A11;
end;
let x be object;
assume x in Z;
then consider W, F being Subset of T such that
A12: x = W\uparrow F and
A13: W in sigma T and
A14: F is finite;
W /\ [#]T = W by XBOOLE_1:28;
then
A15: x = W /\ ([#]T\uparrow F) by A12,XBOOLE_1:49;
reconsider G = F as Subset of R by A2;
A16: (uparrow G)` in B2 by A14;
(uparrow F)` = (uparrow G)` by A2,WAYBEL_0:13;
hence thesis by A16,A13,A15,SETFAM_1:def 5;
end;
A17: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
B2 c= Z
proof
let x be object;
assume x in B2;
then consider F being Subset of R such that
A18: x = (uparrow F)` and
A19: F is finite;
A20: the carrier of S in B1 by A1,PRE_TOPC:def 1;
reconsider G = F as Subset of T by A2;
uparrow F = uparrow G by A2,WAYBEL_0:13;
hence thesis by A17,A20,A2,A18,A19;
end;
then
A21: B2 \/ Z = Z by XBOOLE_1:12;
T is TopAugmentation of T by YELLOW_9:44;
then T is Refinement of S,R by Th29;
then B1 \/ B2 \/ INTERSECTION(B1,B2) is Basis of T by YELLOW_9:59;
hence thesis by A4,A5,A21,XBOOLE_1:4;
end;
definition :: 1.5. DEFINITION, p. 144 (part II)
let T be complete LATTICE;
func lambda T -> Subset-Family of T means
: Def4:
for S being Lawson correct TopAugmentation of T holds it = the topology of S;
uniqueness
proof
set S = the Lawson correct TopAugmentation of T;
let L1,L2 be Subset-Family of T;
assume for S being Lawson correct TopAugmentation of T holds L1 = the
topology of S;
then L1 = the topology of S;
hence thesis;
end;
existence
proof
set S = the Lawson correct TopAugmentation of T;
A1: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then reconsider t = the topology of S as Subset-Family of T;
take t;
let S9 be Lawson correct TopAugmentation of T;
A2: the RelStr of S9 = the RelStr of T by YELLOW_9:def 4;
then
A3: sigma S9 = sigma S by A1,YELLOW_9:52;
(omega S9) \/ sigma S9 is prebasis of S9 by Def3;
then
A4: FinMeetCl ((omega S9) \/ sigma S9) is Basis of S9 by YELLOW_9:23;
A5: omega S9 = omega S by A2,A1,Th3;
(omega S) \/ sigma S is prebasis of S by Def3;
then FinMeetCl ((omega S) \/ sigma S) is Basis of S by YELLOW_9:23;
hence t = UniCl FinMeetCl ((omega S) \/ sigma S) by YELLOW_9:22
.= the topology of S9 by A1,A2,A5,A3,A4,YELLOW_9:22;
end;
end;
theorem Th33:
for R being complete LATTICE holds lambda R = UniCl FinMeetCl ((
sigma R) \/ (omega R))
proof
let R be complete LATTICE;
set S = the Lawson correct TopAugmentation of R;
A1: the RelStr of S = the RelStr of R by YELLOW_9:def 4;
then
A2: sigma R = sigma S by YELLOW_9:52;
(omega S) \/ sigma S is prebasis of S by Def3;
then FinMeetCl ((omega S) \/ sigma S) is Basis of S by YELLOW_9:23;
then
A3: the topology of S = UniCl FinMeetCl ((omega S) \/ sigma S) by YELLOW_9:22;
omega R = omega S by A1,Th3;
hence thesis by A3,A1,A2,Def4;
end;
theorem
for R being complete LATTICE for T being lower correct TopAugmentation
of R for S being Scott correct TopAugmentation of R for M being Refinement of S
,T holds lambda R = the topology of M
proof
let R be complete LATTICE;
let T be lower correct TopAugmentation of R;
let S be Scott correct TopAugmentation of R;
let M be Refinement of S,T;
A1: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
A2: (the carrier of R) \/ the carrier of R = the carrier of R;
the RelStr of S = the RelStr of R by YELLOW_9:def 4;
then
A3: the carrier of M = the carrier of R by A2,A1,YELLOW_9:def 6;
A4: sigma R = the topology of S by YELLOW_9:51;
omega R = the topology of T by Def2;
then (sigma R) \/ omega R is prebasis of M by A4,YELLOW_9:def 6;
then
A5: FinMeetCl ((sigma R) \/ omega R) is Basis of M by A3,YELLOW_9:23;
thus lambda R = UniCl FinMeetCl ((sigma R) \/ (omega R)) by Th33
.= the topology of M by A3,A5,YELLOW_9:22;
end;
Lm2: for T being LATTICE, F being Subset-Family of T st for A being Subset of
T st A in F holds A is property(S) holds union F is property(S)
proof
let T be LATTICE, F be Subset-Family of T such that
A1: for A being Subset of T st A in F holds A is property(S);
let D be non empty directed Subset of T;
assume sup D in union F;
then consider A being set such that
A2: sup D in A and
A3: A in F by TARSKI:def 4;
reconsider A as Subset of T by A3;
A is property(S) by A1,A3;
then consider y being Element of T such that
A4: y in D and
A5: for x being Element of T st x in D & x >= y holds x in A by A2;
take y;
thus y in D by A4;
let x be Element of T;
assume that
A6: x in D and
A7: x >= y;
x in A by A6,A7,A5;
hence thesis by A3,TARSKI:def 4;
end;
Lm3: for T being LATTICE for A1,A2 being Subset of T st A1 is property(S) & A2
is property(S) holds A1 /\ A2 is property(S)
proof
let T be LATTICE, A1,A2 be Subset of T such that
A1: for D being non empty directed Subset of T st sup D in A1 ex y being
Element of T st y in D & for x being Element of T st x in D & x >= y holds x in
A1 and
A2: for D being non empty directed Subset of T st sup D in A2 ex y being
Element of T st y in D & for x being Element of T st x in D & x >= y holds x in
A2;
let D be non empty directed Subset of T;
assume
A3: sup D in A1 /\ A2;
then sup D in A1 by XBOOLE_0:def 4;
then consider y1 being Element of T such that
A4: y1 in D and
A5: for x being Element of T st x in D & x >= y1 holds x in A1 by A1;
sup D in A2 by A3,XBOOLE_0:def 4;
then consider y2 being Element of T such that
A6: y2 in D and
A7: for x being Element of T st x in D & x >= y2 holds x in A2 by A2;
consider y being Element of T such that
A8: y in D and
A9: y1 <= y and
A10: y2 <= y by A4,A6,WAYBEL_0:def 1;
take y;
thus y in D by A8;
let x be Element of T;
assume that
A11: x in D and
A12: x >= y;
A13: x in A2 by A12,A10,A7,A11,ORDERS_2:3;
x in A1 by A12,A9,A5,A11,ORDERS_2:3;
hence thesis by A13,XBOOLE_0:def 4;
end;
Lm4: for T being LATTICE holds [#]T is property(S)
proof
let T be LATTICE;
let D be non empty directed Subset of T such that
sup D in [#]T;
set y = the Element of D;
reconsider y as Element of T;
take y;
thus thesis;
end;
theorem Th35:
for T being lower up-complete TopLattice for A being Subset of T
st A is open holds A is property(S)
proof
let T be lower up-complete TopLattice;
defpred P[Subset of T] means $1 is property(S);
A1: ex K being prebasis of T st for A being Subset of T st A in K holds P[A]
proof
reconsider K = the set of all (uparrow x)` where x is Element of T
as prebasis of T by Def1;
take K;
let A be Subset of T;
assume A in K;
then consider x being Element of T such that
A2: A = (uparrow x)`;
let D be non empty directed Subset of T;
assume
A3: sup D in A;
set y = the Element of D;
reconsider y as Element of T;
take y;
thus y in D;
let z be Element of T;
assume that
A4: z in D and
z >= y and
A5: not z in A;
A6: z >= x by A5,A2,YELLOW_9:1;
not x <= sup D by A3,A2,YELLOW_9:1;
then
A7: not z <= sup D by A6,ORDERS_2:3;
A8: ex_sup_of D,T by WAYBEL_0:75;
A9: ex_sup_of {z},T by YELLOW_0:38;
{z} c= D by A4,ZFMISC_1:31;
then sup {z} <= sup D by A8,A9,YELLOW_0:34;
hence thesis by A7,YELLOW_0:39;
end;
A10: for A1,A2 being Subset of T st P[A1] & P[A2] holds P[A1 /\ A2] by Lm3;
A11: P[[#]T] by Lm4;
A12: for F being Subset-Family of T st for A being Subset of T st A in F
holds P[A] holds P[union F] by Lm2;
thus for A being Subset of T st A is open holds P[A] from TopInd(A1,A12,A10,
A11);
end;
theorem Th36:
:: Remark after 1.5. p. 144
for T being Lawson complete TopLattice for A being Subset of T
st A is open holds A is property(S)
proof
let T be Lawson complete TopLattice;
defpred P[Subset of T] means $1 is property(S);
set S = the Scott TopAugmentation of T,R = the lower correct TopAugmentation of
T;
A1: the RelStr of R = the RelStr of T by YELLOW_9:def 4;
A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
A3: ex K being prebasis of T st for A being Subset of T st A in K holds P[A]
proof
reconsider K = (sigma T) \/ omega T as prebasis of T by Def3;
take K;
let A be Subset of T;
reconsider AS = A as Subset of S by A2;
reconsider AR = A as Subset of R by A1;
assume A in K;
then
A in sigma T & sigma T = the topology of S or A in omega T & omega T =
the topology of R by Def2,XBOOLE_0:def 3,YELLOW_9:51;
then AS is open or AR is open;
then AS is property(S) or AR is property(S) by Th35,WAYBEL11:15;
hence thesis by A2,A1,YELLOW12:19;
end;
A4: P[[#]T];
A5: for A1,A2 being Subset of T st P[A1] & P[A2] holds P[A1 /\ A2] by Lm3;
A6: for F being Subset-Family of T st for A being Subset of T st A in F
holds P[A] holds P[union F] by Lm2;
thus for A being Subset of T st A is open holds P[A] from TopInd(A3,A6,A5,
A4);
end;
theorem Th37:
for S being Scott complete TopLattice for T being Lawson correct
TopAugmentation of S for A being Subset of S st A is open for C being Subset of
T st C = A holds C is open
proof
let S be Scott complete TopLattice;
let T be Lawson correct TopAugmentation of S;
let A be Subset of S;
assume
A1: A in the topology of S;
let C be Subset of T;
assume
A2: C = A;
(sigma T) \/ omega T is prebasis of T by Def3;
then
A3: (sigma T) \/ omega T c= the topology of T by TOPS_2:64;
the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then S is Scott TopAugmentation of T by YELLOW_9:def 4;
then A in sigma T by A1,YELLOW_9:51;
then C in (sigma T) \/ omega T by A2,XBOOLE_0:def 3;
hence C in the topology of T by A3;
end;
theorem Th38:
for T being Lawson complete TopLattice
for x being Element of T holds
uparrow x is closed & downarrow x is closed & {x} is closed
proof let T be Lawson complete TopLattice;
set S = the Scott TopAugmentation of T;
set R = the lower correct TopAugmentation of T;
A: the RelStr of S = the RelStr of T & the RelStr of R = the RelStr of T
by YELLOW_9:def 4;
T is TopAugmentation of T by YELLOW_9:44; then
C: T is Refinement of S,R by Th29; then
D: T is Refinement of R,S by YELLOW_9:55;
let x be Element of T;
reconsider y = x as Element of S by A;
reconsider z = x as Element of R by A;
downarrow y = downarrow x & downarrow y is closed &
uparrow z = uparrow x & uparrow z is closed
by A,WAYBEL_0:13,Th4,WAYBEL11:11;
hence uparrow x is closed & downarrow x is closed by A,C,D,Th21;
then (uparrow x) /\ downarrow x is closed;
hence thesis by Th28;
end;
theorem Th39:
for T being Lawson complete TopLattice for x being Element of
T holds (uparrow x)` is open & (downarrow x)` is open & {x}` is open
proof
let T be Lawson complete TopLattice;
let x be Element of T;
A1: downarrow x is closed by Th38;
A2: {x} is closed by Th38;
uparrow x is closed by Th38;
hence thesis by A1,A2;
end;
theorem Th40:
for T being Lawson complete continuous TopLattice for x being
Element of T holds wayabove x is open & (wayabove x)` is closed
proof
let T be Lawson continuous complete TopLattice;
let x be Element of T;
set S = the Scott TopAugmentation of T;
A1: T is TopAugmentation of S by YELLOW_9:45;
A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then reconsider v = x as Element of S;
wayabove v is open by WAYBEL11:36;
hence wayabove x is open by A2,A1,Th37,YELLOW12:13;
hence thesis;
end;
theorem
:: 1.6. PROPOSITION (i), p. 144
for S being Scott complete TopLattice for T being Lawson correct
TopAugmentation of S for A being upper Subset of T st A is open for C being
Subset of S st C = A holds C is open
proof
let S be Scott complete TopLattice;
let T be Lawson correct TopAugmentation of S;
let A be upper Subset of T;
assume
A1: A is open;
let C be Subset of S;
A2: the RelStr of T = the RelStr of S by YELLOW_9:def 4;
assume C = A;
then C is upper property(S) by A1,Th36,A2,WAYBEL_0:25,YELLOW12:19;
hence thesis by WAYBEL11:15;
end;
theorem
:: 1.6. PROPOSITION (ii), p. 144
for T being Lawson complete TopLattice for A being lower Subset of T
holds A is closed iff A is closed_under_directed_sups
proof
let T be Lawson complete TopLattice;
let A be lower Subset of T;
set S = the Scott TopAugmentation of T;
hereby
assume A is closed;
then A` is open;
then reconsider mA = A` as property(S) Subset of T by Th36;
mA` = A;
hence A is directly_closed;
end;
assume A is directly_closed;
then reconsider dA = A as directly_closed lower Subset of T;
A1: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then reconsider mA = dA` as Subset of S;
mA is upper inaccessible by A1,WAYBEL_0:25,YELLOW_9:47;
then
A2: mA is open by WAYBEL11:def 4;
T is TopAugmentation of S by A1,YELLOW_9:def 4;
then dA` is open by A2,Th37;
hence thesis;
end;
theorem
:: 1.7. LEMMA, p. 145
for T being Lawson complete TopLattice for F being non empty
filtered Subset of T holds Lim (F opp+id) = {inf F}
proof
let T be Lawson complete TopLattice;
reconsider K = (sigma T) \/ the set of all
(uparrow x)` where x is Element of T as prebasis of T by Th30;
set S = the Scott TopAugmentation of T;
let F be non empty filtered Subset of T;
set N = F opp+id;
A1: the carrier of N = F by YELLOW_9:7;
A2: N is full SubRelStr of T opp by YELLOW_9:7;
thus Lim N c= {inf F}
proof
let p be object;
assume
A3: p in Lim N;
then reconsider p as Element of T;
the mapping of N = id F by Th27;
then rng the mapping of N = F by RELAT_1:45;
then
A4: p in Cl F by A3,WAYBEL_9:24;
p is_<=_than F
proof
let u be Element of T;
assume
A5: u in F;
A6: N is_eventually_in downarrow u
proof
reconsider i = u as Element of N by A5,YELLOW_9:7;
take i;
let j be Element of N;
j in F by A1;
then reconsider z = j as Element of T;
assume j >= i;
then z~ >= u~ by A2,YELLOW_0:59;
then z <= u by LATTICE3:9;
then z in downarrow u by WAYBEL_0:17;
hence thesis by YELLOW_9:7;
end;
downarrow u is closed by Th38;
then Cl downarrow u = downarrow u by PRE_TOPC:22;
then Lim N c= downarrow u by A6,Th26;
hence thesis by A3,WAYBEL_0:17;
end;
then
A7: p <= inf F by YELLOW_0:33;
inf F is_<=_than F by YELLOW_0:33;
then
A8: F c= uparrow inf F by YELLOW_2:2;
uparrow inf F is closed by Th38;
then Cl uparrow inf F = uparrow inf F by PRE_TOPC:22;
then Cl F c= uparrow inf F by A8,PRE_TOPC:19;
then p >= inf F by A4,WAYBEL_0:18;
then p = inf F by A7,ORDERS_2:2;
hence thesis by TARSKI:def 1;
end;
A9: the topology of S = sigma T by YELLOW_9:51;
A10: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
now
let A be Subset of T;
assume that
A11: inf F in A and
A12: A in K;
per cases by A12,XBOOLE_0:def 3;
suppose
A13: A in sigma T;
then reconsider a = A as Subset of S by A9;
set i = the Element of N;
a is open by A9,A13;
then a is upper by WAYBEL11:def 4;
then
A14: A is upper by A10,WAYBEL_0:25;
thus N is_eventually_in A
proof
take i;
let j be Element of N;
j in F by A1;
then reconsider z = j as Element of T;
z >= inf F by A1,YELLOW_2:22;
then z in A by A11,A14;
hence thesis by YELLOW_9:7;
end;
end;
suppose
A in the set of all (uparrow x)` where x is Element of T;
then consider x being Element of T such that
A15: A = (uparrow x)`;
not inf F >= x by A11,A15,YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A16: y in F and
A17: not y >= x;
thus N is_eventually_in A
proof
reconsider i = y as Element of N by A16,YELLOW_9:7;
take i;
let j be Element of N;
j in F by A1;
then reconsider z = j as Element of T;
assume j >= i;
then z~ >= y~ by A2,YELLOW_0:59;
then z <= y by LATTICE3:9;
then not z >= x by A17,ORDERS_2:3;
then z in A by A15,YELLOW_9:1;
hence thesis by YELLOW_9:7;
end;
end;
end;
then inf F in Lim N by Th25;
hence thesis by ZFMISC_1:31;
end;
registration
:: 1.9. THEOREM, p. 146
cluster Lawson -> T_1 compact for complete TopLattice;
coherence
proof
let T be complete TopLattice such that
A1: T is Lawson;
for x be Point of T holds {x} is closed by A1,Th38;
hence T is T_1 by URYSOHN1:19;
set O1 = sigma T, O2 = the set of all (uparrow x)` where x is Element of T;
reconsider K = O1 \/ O2 as prebasis of T by A1,Th30;
set S = the Scott TopAugmentation of T;
the carrier of InclPoset the topology of T = the topology of T by
YELLOW_1:1;
then reconsider
X = the carrier of T as Element of InclPoset the topology of T
by PRE_TOPC:def 1;
A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
for F being Subset of K st X c= union F ex G being finite Subset of F
st X c= union G
proof
deffunc F(Element of T) = (uparrow $1)`;
let F be Subset of K;
set I2 = {x where x is Element of T: (uparrow x)` in F};
set x = "\/"(I2, T);
A3: I2 c= the carrier of T
proof
let a be object;
assume a in I2;
then ex x being Element of T st a = x & (uparrow x)` in F;
hence thesis;
end;
reconsider z = x as Element of S by A2;
assume
A4: X c= union F;
x in X;
then consider Y being set such that
A5: x in Y and
A6: Y in F by A4,TARSKI:def 4;
Y in K by A6;
then reconsider I2, Y as Subset of T by A3;
reconsider Z = Y, J2 = I2 as Subset of S by A2;
now
assume not Y in O1;
then Y in O2 by A6,XBOOLE_0:def 3;
then consider y being Element of T such that
A7: Y = (uparrow y)`;
y in I2 by A6,A7;
then y <= x by YELLOW_2:22;
hence contradiction by A5,A7,YELLOW_9:1;
end;
then Z in the topology of S by YELLOW_9:51;
then
A8: Z is open;
then
A9: Z is upper by WAYBEL11:15;
A10: z = sup J2 by A2,YELLOW_0:17,26
.= sup finsups J2 by WAYBEL_0:55;
Z is property(S) by A8,WAYBEL11:15;
then consider y being Element of S such that
A11: y in finsups J2 and
A12: for x being Element of S st x in finsups J2 & x >= y holds x in
Z by A10,A5;
consider a being finite Subset of J2 such that
A13: y = "\/"(a,S) and
ex_sup_of a,S by A11;
set AA = {(uparrow c)` where c is Element of T: c in a}, G = {Y} \/ AA;
A14: G c= F
proof
let i be object;
assume that
A15: i in G and
A16: not i in F;
i in {Y} or i in AA by A15,XBOOLE_0:def 3;
then consider c being Element of T such that
A17: i = (uparrow c)` and
A18: c in a by A6,A16,TARSKI:def 1;
c in J2 by A18;
then ex c9 being Element of T st c = c9 & (uparrow c9)` in F;
hence contradiction by A16,A17;
end;
A19: a is finite;
{F(c) where c is Element of T: c in a} is finite from FRAENKEL:sch
21(A19);
then reconsider G as finite Subset of F by A14;
take G;
let u be object;
assume that
A20: u in X and
A21: not u in union G;
reconsider u as Element of S by A20,A2;
A22: union G = (union {Y}) \/ union AA by ZFMISC_1:78
.= Y \/ union AA by ZFMISC_1:25;
then
A23: not u in Y by A21,XBOOLE_0:def 3;
A24: not u in union AA by A22,A21,XBOOLE_0:def 3;
A25: y <= y & u is_>=_than a
proof
thus y <= y;
let v be Element of S;
assume
A26: v in a;
then v in J2;
then consider c being Element of T such that
A27: v = c and
(uparrow c)` in F;
(uparrow c)` in AA by A26,A27;
then
A28: not u in (uparrow c)` by A24,TARSKI:def 4;
(uparrow c)` = (uparrow v)` by A2,A27,WAYBEL_0:13;
hence thesis by A28,YELLOW_9:1;
end;
then
A29: u >= y by A13,YELLOW_0:32;
y in Z by A25,A11,A12;
hence thesis by A29,A9,A23;
end;
then X << X by WAYBEL_7:31;
then X is compact;
hence thesis by WAYBEL_3:37;
end;
end;
registration
:: 1.10. THEOREM, p. 146
cluster Lawson -> Hausdorff for complete continuous TopLattice;
coherence
proof
let T be complete continuous TopLattice such that
A1: T is Lawson;
let x, y be Point of T such that
A2: x <> y;
reconsider x9 = x, y9 = y as Element of T;
A3: for x being Element of T holds waybelow x is non empty directed;
per cases by A2,ORDERS_2:2;
suppose
not y9 <= x9;
then consider u being Element of T such that
A4: u << y9 and
A5: not u <= x9 by A3,WAYBEL_3:24;
take V = (uparrow u)`, W = wayabove u;
thus V is open & W is open by A1,Th39,Th40;
thus x in V by A5,YELLOW_9:1;
thus y in W by A4;
A6: V` = uparrow u;
W c= uparrow u by WAYBEL_3:11;
hence thesis by A6,SUBSET_1:23;
end;
suppose
not x9 <= y9;
then consider u being Element of T such that
A7: u << x9 and
A8: not u <= y9 by A3,WAYBEL_3:24;
take W = wayabove u, V = (uparrow u)`;
thus W is open & V is open by A1,Th39,Th40;
thus x in W by A7;
thus y in V by A8,YELLOW_9:1;
A9: V` = uparrow u;
W c= uparrow u by WAYBEL_3:11;
hence thesis by A9,SUBSET_1:23;
end;
end;
end;