:: Introduction to Meet-Continuous Topological Lattices
:: by Artur Korni{\l}owicz
::
:: Received November 3, 1998
:: Copyright (c) 1998-2017 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 STRUCT_0, XBOOLE_0, ZFMISC_1, ORDERS_2, WAYBEL_9, PRE_TOPC,
FINSET_1, SUBSET_1, RCOMP_1, TARSKI, NATTRA_1, CARD_5, RELAT_2, FUNCT_1,
WAYBEL_0, RELAT_1, SEQM_3, XXREAL_0, YELLOW_2, YELLOW_1, CARD_FIL,
ORDINAL2, WELLORD1, WAYBEL_1, FUNCT_2, REWRITE1, LATTICES, YELLOW_0,
LATTICE3, TDLAT_3, RLVECT_3, SETFAM_1, YELLOW_8, TOPS_1, CONNSP_2,
PRELAMB, CANTOR_1, WAYBEL_2, YELLOW13, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPS_2, FUNCT_1, RELSET_1,
BINOP_1, FUNCT_2, FINSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, ORDERS_2,
PRE_TOPC, TOPS_1, COMPTS_1, TDLAT_2, TDLAT_3, LATTICE3, CANTOR_1,
CONNSP_2, BORSUK_1, YELLOW_0, WAYBEL_0, YELLOW_1, ORDERS_3, WAYBEL_1,
YELLOW_2, YELLOW_3, WAYBEL_2, YELLOW_8, WAYBEL_9;
constructors SETFAM_1, TOPS_1, BORSUK_1, URYSOHN1, LATTICE3, TDLAT_2, TDLAT_3,
T_0TOPSP, CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_9, YELLOW_8, COMPTS_1,
TOPS_2, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC,
TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_1,
YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_9, YELLOW11, YELLOW12, RELAT_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, LATTICE3, PRE_TOPC, TOPS_2, WAYBEL_0, WAYBEL_1, YELLOW_8,
BORSUK_1, XBOOLE_0, COMPTS_1;
equalities STRUCT_0, SUBSET_1, BINOP_1;
expansions TARSKI, LATTICE3, PRE_TOPC, BORSUK_1, XBOOLE_0, COMPTS_1;
theorems TARSKI, PRE_TOPC, ORDERS_2, TOPS_1, WAYBEL_3, CONNSP_2, TDLAT_3,
SETFAM_1, COMPTS_1, CANTOR_1, ZFMISC_1, YELLOW_0, YELLOW_2, YELLOW_3,
YELLOW_8, WAYBEL_1, WAYBEL14, YELLOW_9, URYSOHN1, YELLOW_4, WAYBEL_0,
RELAT_1, TDLAT_2, FUNCT_1, FUNCT_2, ORDERS_3, BORSUK_1, TEX_1, WAYBEL_2,
XBOOLE_0, XBOOLE_1, SUBSET_1, TOPS_2;
schemes FINSET_1;
begin :: Preliminaries
theorem Th1:
for T being T_1 non empty TopSpace, A being finite Subset of T
holds A is closed
proof
let T be T_1 non empty TopSpace, A be finite Subset of T;
defpred P[set] means ex S being Subset of T st $1 = S & S is closed;
A1: P[{}]
proof
take {}T;
thus {}T = {};
thus thesis;
end;
A2: for x, C being set st x in A & C c= A & P[C] holds P[C \/ {x}]
proof
let x, C be set;
assume that
A3: x in A and
C c= A and
A4: P[C];
reconsider y = x as Element of T by A3;
consider S being Subset of T such that
A5: C = S and
A6: S is closed by A4;
{y} is closed by URYSOHN1:19;
then S \/ {y} is closed by A6;
hence thesis by A5;
end;
A7: A is finite;
P[A] from FINSET_1:sch 2(A7,A1,A2);
hence thesis;
end;
registration
let T be T_1 non empty TopSpace;
cluster finite -> closed for Subset of T;
coherence by Th1;
end;
registration
let T be compact TopStruct;
cluster [#]T -> compact;
coherence by COMPTS_1:1;
end;
registration
cluster finite T_1 -> discrete for non empty TopSpace;
coherence
proof
let T be non empty TopSpace;
assume T is finite T_1;
then for A being Subset of T holds A is closed;
hence thesis by TDLAT_3:16;
end;
end;
registration
cluster finite -> compact for TopSpace;
coherence;
end;
theorem Th2:
for T being discrete non empty TopSpace holds T is normal
proof
let T be discrete non empty TopSpace;
let W, V be Subset of T such that
W <> {} and
V <> {} and
W is closed and
V is closed and
A1: W /\ V = {};
take P = W, Q = V;
thus P is open & Q is open by TDLAT_3:15;
thus W c= P & V c= Q & P /\ Q = {} by A1;
end;
theorem Th3:
for T being discrete non empty TopSpace holds T is regular
proof
let T be discrete non empty TopSpace;
let p be Point of T, P be Subset of T such that
P <> {} and
P is closed and
A1: p in P`;
take W = {p}, V = P;
thus W is open & V is open by TDLAT_3:15;
A2: not p in P by A1,XBOOLE_0:def 5;
W /\ V c= {}
proof
let a be object;
assume
A3: a in W /\ V;
assume not a in {};
a in W & a in V by A3,XBOOLE_0:def 4;
hence contradiction by A2,TARSKI:def 1;
end;
hence p in W & P c= V & W /\ V = {} by TARSKI:def 1;
end;
theorem Th4:
for T being discrete non empty TopSpace holds T is T_2
proof
let T be discrete non empty TopSpace;
let p, q be Point of T such that
A1: not p = q;
take W = {p}, V = {q};
thus W is open & V is open by TDLAT_3:15;
W /\ V c= {}
proof
let a be object;
assume
A2: a in W /\ V;
then a in W by XBOOLE_0:def 4;
then
A3: a = p by TARSKI:def 1;
assume not a in {};
a in V by A2,XBOOLE_0:def 4;
hence contradiction by A1,A3,TARSKI:def 1;
end;
hence p in W & q in V & W /\ V = {} by TARSKI:def 1;
end;
theorem Th5:
for T being discrete non empty TopSpace holds T is T_1
proof
let T be discrete non empty TopSpace;
for p being Point of T holds {p} is closed by TDLAT_3:16;
hence thesis by URYSOHN1:19;
end;
registration
cluster discrete non empty -> normal regular T_2 T_1 for TopSpace;
coherence by Th2,Th3,Th4,Th5;
end;
registration
cluster T_4 -> regular for non empty TopSpace;
coherence
proof
let T be non empty TopSpace such that
A1: T is T_4;
let p be Point of T, P be Subset of T such that
A2: P <> {} & P is closed and
A3: p in P`;
A4: not p in P by A3,XBOOLE_0:def 5;
P /\ {p} c= {}
proof
let a be object;
assume
A5: a in P /\ {p};
assume not a in {};
a in P & a in {p} by A5,XBOOLE_0:def 4;
hence contradiction by A4,TARSKI:def 1;
end;
then P /\ {p} = {};
then P misses {p};
then consider R, Q being Subset of T such that
A6: R is open & Q is open & {p} c= R & P c= Q & R misses Q by A1,A2,
COMPTS_1:def 3;
take R, Q;
p in {p} by TARSKI:def 1;
hence thesis by A6;
end;
end;
registration
cluster T_3 -> T_2 for TopSpace;
coherence
proof
let T be TopSpace such that
A1: T is T_3;
let p, q be Point of T;
assume
A2: p <> q;
then
A3: not p in {q} by TARSKI:def 1;
now
assume
A4: the carrier of T = {};
then p = {} by SUBSET_1:def 1;
hence contradiction by A2,A4,SUBSET_1:def 1;
end;
then reconsider T9 = T as non empty TopSpace;
reconsider p,q as Point of T9;
p in {q}` by A3,SUBSET_1:29;
then consider W, V being Subset of T such that
A5: W is open & V is open & p in W & {q} c= V & W misses V by A1,COMPTS_1:def 2
;
take W, V;
q in {q} by TARSKI:def 1;
hence thesis by A5;
end;
end;
theorem Th6:
for S being reflexive RelStr, T being reflexive transitive RelStr
, f being Function of S, T, X being Subset of S holds downarrow (f.:X) c=
downarrow (f.:downarrow X)
proof
let S be reflexive RelStr, T be reflexive transitive RelStr, f be Function
of S, T, X be Subset of S;
f.:X c= f.:downarrow X by RELAT_1:123,WAYBEL_0:16;
hence thesis by YELLOW_3:6;
end;
theorem
for S being reflexive RelStr, T being reflexive transitive RelStr, f
being Function of S, T, X being Subset of S st f is monotone holds downarrow (f
.:X) = downarrow (f.:downarrow X)
proof
let S be reflexive RelStr, T be reflexive transitive RelStr, f be Function
of S, T, X be Subset of S such that
A1: f is monotone;
thus downarrow f.:X c= downarrow f.:downarrow X by Th6;
let a be object;
assume
A2: a in downarrow (f.:downarrow X);
then reconsider T1 = T as non empty reflexive transitive RelStr;
reconsider b = a as Element of T1 by A2;
consider fx being Element of T1 such that
A3: fx >= b and
A4: fx in f.:downarrow X by A2,WAYBEL_0:def 15;
consider x being object such that
A5: x in dom f and
A6: x in downarrow X and
A7: fx = f.x by A4,FUNCT_1:def 6;
reconsider S1 = S as non empty reflexive RelStr by A5;
reconsider x as Element of S1 by A5;
consider y being Element of S1 such that
A8: y >= x and
A9: y in X by A6,WAYBEL_0:def 15;
reconsider f1 = f as Function of S1, T1;
f1.x <= f1.y by A1,A8,ORDERS_3:def 5;
then
A10: b <= f1.y by A3,A7,ORDERS_2:3;
the carrier of T1 <> {};
then dom f = the carrier of S by FUNCT_2:def 1;
then f.y in f.:X by A9,FUNCT_1:def 6;
hence thesis by A10,WAYBEL_0:def 15;
end;
theorem Th8:
for N being non empty Poset holds IdsMap N is one-to-one
proof
let N be non empty Poset;
set f = IdsMap N;
let x, y be Element of N such that
A1: f.x = f.y;
f.x = downarrow x & f.y = downarrow y by YELLOW_2:def 4;
hence thesis by A1,WAYBEL_0:19;
end;
registration
let N be non empty Poset;
cluster IdsMap N -> one-to-one;
coherence by Th8;
end;
theorem Th9:
for N being finite LATTICE holds SupMap N is one-to-one
proof
let N be finite LATTICE;
set f = SupMap N;
let x, y be Element of InclPoset Ids N such that
A1: f.x = f.y;
reconsider X = x, Y = y as Ideal of N by YELLOW_2:41;
A2: f.x = sup X & f.y = sup Y by YELLOW_2:def 3;
X = Y
proof
hereby
let a be object;
A3: sup Y in Y by WAYBEL_3:16;
assume
A4: a in X;
then reconsider b = a as Element of N;
b <= sup Y by A1,A2,A4,YELLOW_0:17,YELLOW_4:1;
hence a in Y by A3,WAYBEL_0:def 19;
end;
let a be object;
A5: sup X in X by WAYBEL_3:16;
assume
A6: a in Y;
then reconsider b = a as Element of N;
b <= sup X by A1,A2,A6,YELLOW_0:17,YELLOW_4:1;
hence thesis by A5,WAYBEL_0:def 19;
end;
hence thesis;
end;
registration
let N be finite LATTICE;
cluster SupMap N -> one-to-one;
coherence by Th9;
end;
theorem
for N being finite LATTICE holds N, InclPoset Ids N are_isomorphic
proof
let N be finite LATTICE;
set I = InclPoset Ids N;
take i = IdsMap N;
N is non empty & I is non empty implies i is one-to-one monotone & ex s
being Function of I,N st s = i" & s is monotone
proof
assume that
N is non empty and
I is non empty;
thus i is one-to-one monotone;
take s = SupMap N;
[i,s] is Galois by WAYBEL_1:57;
then i is onto by WAYBEL_1:24;
then
A1: rng i = the carrier of I by FUNCT_2:def 3;
A2: for y, x being object holds y in rng i & x = s.y iff x in dom i & y = i.x
proof
let y, x be object;
A3: dom i = the carrier of N by FUNCT_2:def 1;
hereby
assume that
A4: y in rng i and
A5: x = s.y;
reconsider Y = y as Element of I by A4;
x = s.Y by A5;
hence x in dom i by A3;
reconsider Y1 = Y as Ideal of N by YELLOW_2:41;
thus i.x = i.sup Y1 by A5,YELLOW_2:def 3
.= downarrow sup Y1 by YELLOW_2:def 4
.= y by WAYBEL14:5,WAYBEL_3:16;
end;
assume that
A6: x in dom i and
A7: y = i.x;
reconsider X = x as Element of N by A6;
A8: y = i.X by A7;
then reconsider Y = y as Ideal of N by YELLOW_2:41;
thus y in rng i by A1,A8;
thus s.y = sup Y by YELLOW_2:def 3
.= sup downarrow X by A7,YELLOW_2:def 4
.= x by WAYBEL_0:34;
end;
dom s = the carrier of I by FUNCT_2:def 1;
hence s = i" by A1,A2,FUNCT_1:32;
thus thesis;
end;
hence thesis by WAYBEL_0:def 38;
end;
theorem Th11:
for N being complete non empty Poset, x being Element of N, X
being non empty Subset of N holds x"/\" preserves_inf_of X
proof
let N be complete non empty Poset, x be Element of N, X be non empty
Subset of N such that
A1: ex_inf_of X,N;
A2: for b being Element of N st b is_<=_than (x"/\").:X holds x"/\".inf X >= b
proof
consider y being object such that
A3: y in X by XBOOLE_0:def 1;
reconsider y as Element of N by A3;
let b be Element of N such that
A4: b is_<=_than (x"/\").:X;
A5: (x"/\").: X = {x"/\"z where z is Element of N: z in X} by WAYBEL_1:61;
then x "/\" y in (x"/\").:X by A3;
then
A6: b <= x "/\" y by A4;
X is_>=_than b
proof
let c be Element of N;
assume c in X;
then x "/\" c in (x"/\").:X by A5;
then
A7: b <= x "/\" c by A4;
x "/\" c <= c by YELLOW_0:23;
hence b <= c by A7,ORDERS_2:3;
end;
then
A8: b <= inf X by A1,YELLOW_0:def 10;
x "/\" y <= x by YELLOW_0:23;
then b <= x by A6,ORDERS_2:3;
then b "/\" b <= x "/\" inf X by A8,YELLOW_3:2;
then b <= x "/\" inf X by YELLOW_0:25;
hence b <= x"/\".inf X by WAYBEL_1:def 18;
end;
thus ex_inf_of (x"/\").:X,N by YELLOW_0:17;
inf X is_<=_than X by A1,YELLOW_0:def 10;
then x"/\".inf X is_<=_than (x"/\").:X by YELLOW_2:13;
hence thesis by A2,YELLOW_0:33;
end;
theorem Th12:
for N being complete non empty Poset, x being Element of N
holds x"/\" is meet-preserving
proof
let N be complete non empty Poset, x be Element of N;
let a, b be Element of N;
thus thesis by Th11;
end;
registration
let N be complete non empty Poset, x be Element of N;
cluster x"/\" -> meet-preserving;
coherence by Th12;
end;
begin :: On the basis of topological spaces
theorem
for T being anti-discrete non empty TopStruct, p being Point of T
holds {the carrier of T} is Basis of p
proof
let T be anti-discrete non empty TopStruct, p be Point of T;
set A = {the carrier of T};
A c= bool the carrier of T
proof
let a be object;
assume a in A;
then
A1: a = the carrier of T by TARSKI:def 1;
the carrier of T c= the carrier of T;
hence thesis by A1;
end;
then reconsider A as Subset-Family of T;
A is Basis of p
proof
A2: A is open
proof
let a be Subset of T;
assume a in A;
then a = [#]T by TARSKI:def 1;
hence thesis;
end;
A is p-quasi_basis
proof
Intersect A = meet A by SETFAM_1:def 9
.= the carrier of T by SETFAM_1:10;
hence p in Intersect A;
let S be Subset of T;
assume S is open & p in S;
then
A3: S = the carrier of T by TDLAT_3:18;
take S;
thus thesis by A3,TARSKI:def 1;
end;
hence thesis by A2;
end;
hence thesis;
end;
theorem
for T being anti-discrete non empty TopStruct, p being Point of T, D
being Basis of p holds D = {the carrier of T}
proof
let T be anti-discrete non empty TopStruct, p be Point of T, D be Basis of p;
thus D c= {the carrier of T}
proof
let a be object;
assume
A1: a in D;
then reconsider X = a as Subset of T;
X is open & p in X by A1,YELLOW_8:12;
then X = the carrier of T by TDLAT_3:18;
hence thesis by TARSKI:def 1;
end;
hence thesis by ZFMISC_1:33;
end;
theorem
for T being non empty TopSpace, P being Basis of T, p being Point of T
holds {A where A is Subset of T: A in P & p in A} is Basis of p
proof
let T be non empty TopSpace, P be Basis of T, p be Point of T;
set Z = {A where A is Subset of T: A in P & p in A};
Z c= bool the carrier of T
proof
let z be object;
assume z in Z;
then ex A being Subset of T st A = z & A in P & p in A;
hence thesis;
end;
then reconsider Z as Subset-Family of T;
reconsider Z as Subset-Family of T;
Z is Basis of p
proof
A1: Z is open
proof
let z be Subset of T;
assume z in Z;
then consider A being Subset of T such that
A2: A = z and
A3: A in P and
p in A;
A is open by A3,YELLOW_8:10;
hence thesis by A2;
end;
Z is p-quasi_basis
proof
now
let z be set;
assume z in Z;
then ex A being Subset of T st A = z & A in P & p in A;
hence p in z;
end;
hence p in Intersect Z by SETFAM_1:43;
let S be Subset of T;
assume S is open & p in S;
then consider V being Subset of T such that
A4: V in P & p in V & V c= S by YELLOW_9:31;
take V;
thus thesis by A4;
end;
hence thesis by A1;
end;
hence thesis;
end;
Lm1: for T being non empty TopStruct, A being Subset of T, p being Point of T
st p in Cl A for K being Basis of p, Q being Subset of T st Q in K holds A
meets Q
proof
let T be non empty TopStruct, A be Subset of T, p be Point of T such that
A1: p in Cl A;
let K be Basis of p, Q be Subset of T;
assume Q in K;
then Q is open & p in Q by YELLOW_8:12;
then A meets Q by A1,PRE_TOPC:def 7;
hence A /\ Q <> {};
end;
Lm2: for T being non empty TopStruct, A being Subset of T, p being Point of T
st for K being Basis of p, Q being Subset of T st Q in K holds A meets Q ex K
being Basis of p st for Q being Subset of T st Q in K holds A meets Q
proof
let T be non empty TopStruct, A be Subset of T, p be Point of T such that
A1: for K being Basis of p, Q being Subset of T st Q in K holds A meets Q and
A2: for K being Basis of p ex Q being Subset of T st Q in K & A misses Q;
set K = the Basis of p;
ex Q being Subset of T st Q in K & A misses Q by A2;
hence contradiction by A1;
end;
Lm3: for T being non empty TopStruct, A being Subset of T, p being Point of T
st ex K being Basis of p st for Q being Subset of T st Q in K holds A meets Q
holds p in Cl A
proof
let T be non empty TopStruct, A be Subset of T, p be Point of T;
given K being Basis of p such that
A1: for Q being Subset of T st Q in K holds A meets Q;
assume not p in Cl A;
then consider F being Subset of T such that
A2: F is closed and
A3: A c= F and
A4: not p in F by PRE_TOPC:15;
A5: A misses F` by A3,SUBSET_1:24;
p in F` & F` is open by A2,A4,XBOOLE_0:def 5;
then consider W being Subset of T such that
A6: W in K and
A7: W c= F` by YELLOW_8:13;
A meets W by A1,A6;
hence contradiction by A7,A5,XBOOLE_1:63;
end;
theorem
for T being non empty TopStruct, A being Subset of T, p being Point of
T holds p in Cl A iff for K being Basis of p, Q being Subset of T st Q in K
holds A meets Q
proof
let T be non empty TopStruct, A be Subset of T, p be Point of T;
thus p in Cl A implies for K being Basis of p, Q being Subset of T st Q in K
holds A meets Q by Lm1;
assume for K being Basis of p, Q being Subset of T st Q in K holds A meets Q;
then
ex K being Basis of p st for Q being Subset of T st Q in K holds A meets
Q by Lm2;
hence thesis by Lm3;
end;
theorem
for T being non empty TopStruct, A being Subset of T, p being Point of
T holds p in Cl A iff ex K being Basis of p st for Q being Subset of T st Q in
K holds A meets Q
proof
let T be non empty TopStruct, A be Subset of T, p be Point of T;
hereby
assume p in Cl A;
then
for K being Basis of p, Q being Subset of T st Q in K holds A meets Q
by Lm1;
hence ex K being Basis of p st for Q being Subset of T st Q in K holds A
meets Q by Lm2;
end;
assume
ex K being Basis of p st for Q being Subset of T st Q in K holds A meets Q;
hence thesis by Lm3;
end;
definition
let T be TopStruct, p be Point of T;
mode basis of p -> Subset-Family of T means
:Def1:
for A being Subset of T
st p in Int A ex P being Subset of T st P in it & p in Int P & P c= A;
existence
proof
reconsider F = bool the carrier of T as Subset-Family of T;
reconsider F as Subset-Family of T;
take F;
let A be Subset of T such that
A1: p in Int A;
take Int A;
thus thesis by A1,TOPS_1:16;
end;
end;
definition
let T be non empty TopSpace, p be Point of T;
redefine mode basis of p means
for A being a_neighborhood of p ex P being
a_neighborhood of p st P in it & P c= A;
compatibility
proof
let F be Subset-Family of T;
hereby
assume
A1: F is basis of p;
let A be a_neighborhood of p;
p in Int A by CONNSP_2:def 1;
then consider P being Subset of T such that
A2: P in F and
A3: p in Int P and
A4: P c= A by A1,Def1;
reconsider P as a_neighborhood of p by A3,CONNSP_2:def 1;
take P;
thus P in F & P c= A by A2,A4;
end;
assume
A5: for A being a_neighborhood of p ex P being a_neighborhood of p st
P in F & P c= A;
let A be Subset of T;
assume p in Int A;
then A is a_neighborhood of p by CONNSP_2:def 1;
then consider P being a_neighborhood of p such that
A6: P in F & P c= A by A5;
take P;
thus thesis by A6,CONNSP_2:def 1;
end;
end;
theorem Th18:
for T being TopStruct, p being Point of T holds bool the carrier
of T is basis of p
proof
let T be TopStruct, p be Point of T;
reconsider F = bool the carrier of T as Subset-Family of T;
reconsider F as Subset-Family of T;
F is basis of p
proof
let A be Subset of T such that
A1: p in Int A;
take Int A;
thus thesis by A1,TOPS_1:16;
end;
hence thesis;
end;
theorem Th19:
for T being non empty TopSpace, p being Point of T, P being
basis of p holds P is non empty
proof
let T be non empty TopSpace, p be Point of T, P be basis of p;
Int [#]T = [#]T by TOPS_1:15;
then ex W being Subset of T st W in P & p in Int W & W c= [#]T by Def1;
hence thesis;
end;
registration
let T be non empty TopSpace, p be Point of T;
cluster -> non empty for basis of p;
coherence by Th19;
end;
registration
let T be TopStruct, p be Point of T;
cluster non empty for basis of p;
existence
proof
bool the carrier of T is basis of p by Th18;
hence thesis;
end;
end;
definition
let T be TopStruct, p be Point of T, P be basis of p;
attr P is correct means
:Def3:
for A being Subset of T holds A in P iff p in Int A;
end;
Lm4: now
let T be TopStruct, p be Point of T;
let K be set such that
A1: K = {A where A is Subset of T: p in Int A};
K c= bool the carrier of T
proof
let y be object;
assume y in K;
then ex A being Subset of T st y = A & p in Int A by A1;
hence thesis;
end;
then reconsider J = K as Subset-Family of T;
reconsider J as Subset-Family of T;
for A being Subset of T st p in Int A ex P being Subset of T st P in J &
p in Int P & P c= A
proof
let A be Subset of T such that
A2: p in Int A;
take P = A;
thus thesis by A1,A2;
end;
hence K is basis of p by Def1;
end;
Lm5: now
let T be TopStruct, p be Point of T, K be basis of p such that
A1: K = {A where A is Subset of T: p in Int A};
thus K is correct
proof
let A be Subset of T;
hereby
assume A in K;
then ex M being Subset of T st A = M & p in Int M by A1;
hence p in Int A;
end;
thus thesis by A1;
end;
end;
registration
let T be TopStruct, p be Point of T;
cluster correct for basis of p;
existence
proof
reconsider P = {A where A is Subset of T: p in Int A} as basis of p by Lm4;
take P;
thus thesis by Lm5;
end;
end;
theorem
for T being TopStruct, p being Point of T holds {A where A is Subset
of T: p in Int A} is correct basis of p by Lm4,Lm5;
registration
let T be non empty TopSpace, p be Point of T;
cluster non empty correct for basis of p;
existence
proof
reconsider K = {A where A is Subset of T: p in Int A} as correct basis of
p by Lm4,Lm5;
take K;
thus thesis;
end;
end;
theorem
for T being anti-discrete non empty TopStruct, p being Point of T
holds {the carrier of T} is correct basis of p
proof
let T be anti-discrete non empty TopStruct, p be Point of T;
set A = {the carrier of T};
A c= bool the carrier of T
proof
let a be object;
assume a in A;
then
A1: a = the carrier of T by TARSKI:def 1;
the carrier of T c= the carrier of T;
hence thesis by A1;
end;
then reconsider A as Subset-Family of T;
reconsider A as Subset-Family of T;
A is basis of p
proof
let S be a_neighborhood of p;
take S;
p in Int S by CONNSP_2:def 1;
then
A2: Int S = the carrier of T by TDLAT_3:18;
Int S c= S by TOPS_1:16;
then Int S = S by A2;
hence thesis by A2,TARSKI:def 1;
end;
then reconsider A as basis of p;
A is correct
proof
let X be Subset of T;
hereby
assume X in A;
then X = the carrier of T by TARSKI:def 1;
then Int X = [#]T by TOPS_1:15;
hence p in Int X;
end;
assume p in Int X;
then
A3: Int X = the carrier of T by TDLAT_3:18;
Int X c= X by TOPS_1:16;
then Int X = X by A3;
hence thesis by A3,TARSKI:def 1;
end;
hence thesis;
end;
theorem
for T being anti-discrete non empty TopStruct, p being Point of T, D
being correct basis of p holds D = {the carrier of T}
proof
let T be anti-discrete non empty TopStruct, p be Point of T, D be correct
basis of p;
thus D c= {the carrier of T}
proof
let a be object;
assume
A1: a in D;
then reconsider X = a as Subset of T;
p in Int X by A1,Def3;
then
A2: Int X = the carrier of T by TDLAT_3:18;
Int X c= X by TOPS_1:16;
then Int X = X by A2;
hence thesis by A2,TARSKI:def 1;
end;
hence thesis by ZFMISC_1:33;
end;
theorem
for T being non empty TopSpace, p being Point of T, P being Basis of p
holds P is basis of p
proof
let T be non empty TopSpace, p be Point of T, P be Basis of p;
now
let A be Subset of T;
assume p in Int A;
then consider V being Subset of T such that
A1: V in P and
A2: V c= Int A by YELLOW_8:def 1;
take V;
V is open by A1,YELLOW_8:12;
then Int A c= A & Int V = V by TOPS_1:16,23;
hence V in P & p in Int V & V c= A by A1,A2,YELLOW_8:12;
end;
hence thesis by Def1;
end;
definition
let T be TopStruct;
mode basis of T -> Subset-Family of T means
:Def4:
for p being Point of T holds it is basis of p;
existence
proof
reconsider F = bool the carrier of T as Subset-Family of T;
reconsider F as Subset-Family of T;
take F;
thus thesis by Th18;
end;
end;
theorem Th24:
for T being TopStruct holds bool the carrier of T is basis of T
proof
let T be TopStruct;
reconsider P = bool the carrier of T as Subset-Family of T;
reconsider P as Subset-Family of T;
P is basis of T
proof
let p be Point of T;
thus thesis by Th18;
end;
hence thesis;
end;
theorem Th25:
for T being non empty TopSpace, P being basis of T holds P is non empty
proof
let T be non empty TopSpace, P be basis of T;
set p = the Point of T;
reconsider C = P as basis of p by Def4;
C is non empty;
hence thesis;
end;
registration
let T be non empty TopSpace;
cluster -> non empty for basis of T;
coherence by Th25;
end;
registration
let T be TopStruct;
cluster non empty for basis of T;
existence
proof
bool the carrier of T is basis of T by Th24;
hence thesis;
end;
end;
theorem
for T being non empty TopSpace, P being basis of T holds the topology
of T c= UniCl Int P
proof
let T be non empty TopSpace, P be basis of T;
let x be object;
assume
A1: x in the topology of T;
then reconsider X = x as Subset of T;
ex Y being Subset-Family of T st Y c= Int P & X = union Y
proof
set Y = {A where A is Subset of T: A in Int P & Int A c= X};
Y c= bool the carrier of T
proof
let y be object;
assume y in Y;
then ex A being Subset of T st y = A & A in Int P & Int A c= X;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
reconsider Y as Subset-Family of T;
take Y;
hereby
let y be object;
assume y in Y;
then ex A being Subset of T st y = A & A in Int P & Int A c= X;
hence y in Int P;
end;
hereby
let y be object;
assume
A2: y in X;
then reconsider p = y as Point of T;
reconsider C = P as basis of p by Def4;
X is open by A1;
then p in Int X by A2,TOPS_1:23;
then consider W being Subset of T such that
A3: W in C and
A4: p in Int W and
A5: W c= X by Def1;
Int W c= W by TOPS_1:16;
then
A6: Int Int W c= X by A5;
Int W in Int P by A3,TDLAT_2:def 1;
then Int W in Y by A6;
hence y in union Y by A4,TARSKI:def 4;
end;
let y be object;
assume y in union Y;
then consider K being set such that
A7: y in K and
A8: K in Y by TARSKI:def 4;
consider A being Subset of T such that
A9: A = K and
A10: A in Int P and
A11: Int A c= X by A8;
reconsider A as Subset of T;
ex E being Subset of T st A = Int E & E in P by A10,TDLAT_2:def 1;
hence thesis by A7,A9,A11;
end;
hence thesis by CANTOR_1:def 1;
end;
theorem
for T being TopSpace, P being Basis of T holds P is basis of T
proof
let T be TopSpace, P be Basis of T;
A1: P c= the topology of T by TOPS_2:64;
let p be Point of T, A be Subset of T such that
A2: p in Int A;
the topology of T c= UniCl P & Int A in the topology of T by CANTOR_1:def 2
,PRE_TOPC:def 2;
then consider Y being Subset-Family of T such that
A3: Y c= P and
A4: Int A = union Y by CANTOR_1:def 1;
reconsider Y as Subset-Family of T;
consider K being set such that
A5: p in K and
A6: K in Y by A2,A4,TARSKI:def 4;
reconsider K as Subset of T by A6;
take K;
thus K in P by A3,A6;
then K is open by A1;
hence p in Int K by A5,TOPS_1:23;
A7: Int A c= A by TOPS_1:16;
K c= union Y by A6,ZFMISC_1:74;
hence thesis by A4,A7;
end;
definition
let T be non empty TopSpace-like TopRelStr;
attr T is topological_semilattice means
:Def5:
for f being Function of [:T,T qua TopSpace:], T st f = inf_op T
holds f is continuous;
end;
registration
cluster reflexive -> topological_semilattice
for 1-element TopSpace-like TopRelStr;
coherence
proof
let T be 1-element TopSpace-like TopRelStr;
assume T is reflexive;
then reconsider W = T as reflexive 1-element TopSpace-like TopRelStr;
consider d being Element of W such that
A1: the carrier of W = {d} by TEX_1:def 1;
let f be Function of [:T,T qua TopSpace:], T such that
A2: f = inf_op T;
now
let P1 be Subset of T such that
P1 is closed;
per cases by TDLAT_3:19;
suppose
P1 = {};
then f"P1 = {}[:T,T qua TopSpace:];
hence f"P1 is closed;
end;
suppose
A3: P1 = the carrier of W;
A4: dom f = the carrier of [:T,T qua TopSpace:] by FUNCT_2:def 1
.= [:the carrier of T,the carrier of T:] by BORSUK_1:def 2;
A5: f"P1 = [:{d},{d}:]
proof
thus for x being object st x in f"P1 holds x in [:{d},{d}:]
by A1,A4,
FUNCT_1:def 7;
let x be object;
A6: [d,d] in [:the carrier of T,the carrier of T:] by ZFMISC_1:87;
assume x in [:{d},{d}:];
then x in {[d,d]} by ZFMISC_1:29;
then
A7: x = [d,d] by TARSKI:def 1;
f.(d,d) = d "/\" d by A2,WAYBEL_2:def 4
.= d by YELLOW_0:25;
hence thesis by A3,A4,A7,A6,FUNCT_1:def 7;
end;
[#][:T,T qua TopSpace:] = [:{d},{d}:] by A1,BORSUK_1:def 2;
hence f"P1 is closed by A5;
end;
end;
hence thesis;
end;
end;
theorem Th28:
for T being topological_semilattice non empty TopSpace-like
TopRelStr, x being Element of T holds x"/\" is continuous
proof
let T be topological_semilattice non empty TopSpace-like TopRelStr, x be
Element of T;
let p be Point of T, G be a_neighborhood of x"/\".p;
set TT = [:T,T qua TopSpace:];
A1: the carrier of TT = [:the carrier of T,the carrier of T:]
by BORSUK_1:def 2;
then reconsider xp = [x,p] as Point of TT by YELLOW_3:def 2;
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by
YELLOW_3:def 2;
then reconsider f = inf_op T as Function of TT, T by A1;
A2: f.xp = f.(x,p) .= x "/\" p by WAYBEL_2:def 4;
G is a_neighborhood of x"/\"p & f is continuous by Def5,WAYBEL_1:def 18;
then consider H being a_neighborhood of xp such that
A3: f.:H c= G by A2;
consider A being Subset-Family of TT such that
A4: Int H = union A and
A5: for e being set st e in A ex X1, Y1 being Subset of T st e = [:X1,Y1
:] & X1 is open & Y1 is open by BORSUK_1:5;
xp in Int H by CONNSP_2:def 1;
then consider Z being set such that
A6: xp in Z and
A7: Z in A by A4,TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A8: Z = [:X1,Y1:] and
X1 is open and
A9: Y1 is open by A5,A7;
p in Y1 by A6,A8,ZFMISC_1:87;
then reconsider Y1 as a_neighborhood of p by A9,CONNSP_2:3;
take Y1;
let b be object;
assume b in (x"/\").:Y1;
then consider a being object such that
a in dom (x"/\") and
A10: a in Y1 and
A11: b = x"/\".a by FUNCT_1:def 6;
reconsider a as Element of T by A10;
x in X1 by A6,A8,ZFMISC_1:87;
then [x,a] in Z by A8,A10,ZFMISC_1:87;
then
A12: [x,a] in Int H by A4,A7,TARSKI:def 4;
[x,a] in [:the carrier of T,the carrier of T:] by ZFMISC_1:87;
then
A13: Int H c= H & [x,a] in dom f by A1,FUNCT_2:def 1,TOPS_1:16;
b = x "/\" a by A11,WAYBEL_1:def 18
.= f.(x,a) by WAYBEL_2:def 4;
then b in f.:H by A12,A13,FUNCT_1:def 6;
hence thesis by A3;
end;
registration
let T be topological_semilatticenon empty TopSpace-like TopRelStr, x be
Element of T;
cluster x"/\" -> continuous;
coherence by Th28;
end;