:: Bases and Refinements of Topologies
:: by Grzegorz Bancerek
::
:: Received March 9, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, ORDERS_2, SETFAM_1, WAYBEL_0, XXREAL_0,
STRUCT_0, PRE_TOPC, FUNCT_1, RELAT_1, TARSKI, REWRITE1, ZFMISC_1,
WAYBEL_9, RELAT_2, NATTRA_1, FINSET_1, LATTICES, FUNCOP_1, YELLOW_0,
ORDINAL2, FUNCT_3, SEQM_3, CAT_1, WELLORD1, ARYTM_0, RLVECT_3, CANTOR_1,
FUNCT_2, RCOMP_1, CONNSP_2, TOPS_1, LATTICE3, BORSUK_1, PRELAMB,
CARD_FIL, PROB_1, YELLOW_6, WAYBEL11, YELLOW_9, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FINSET_1, MCART_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1,
STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0,
TDLAT_3, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, YELLOW_6, YELLOW_7,
WAYBEL_9, WAYBEL11, CANTOR_1, BORSUK_1;
constructors SETFAM_1, TOLER_1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3,
CANTOR_1, ORDERS_3, WAYBEL11, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0,
BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_2,
YELLOW_6, WAYBEL_9, WAYBEL11, FUNCT_2, CANTOR_1, RELSET_1;
requirements BOOLE, SUBSET;
begin :: Subsets as nets
scheme :: YELLOW_9:sch 1
FraenkelInvolution
{A() -> non empty set, X,Y() -> Subset of A(), F(set) -> Element of A()}:
X() = {F(a) where a is Element of A(): a in Y()}
provided
Y() = {F(a) where a is Element of A(): a in X()} and
for a being Element of A() holds F(F(a)) = a;
scheme :: YELLOW_9:sch 2
FraenkelComplement1
{A() -> non empty RelStr, X() -> Subset-Family of A(), Y() -> set,
F(set) -> Subset of A()}:
COMPLEMENT X() = {F(a)` where a is Element of A(): a in Y()}
provided
X() = {F(a) where a is Element of A(): a in Y()};
scheme :: YELLOW_9:sch 3
FraenkelComplement2
{A() -> non empty RelStr, X() -> Subset-Family of A(), Y() -> set,
F(set) -> Subset of A()}:
COMPLEMENT X() = {F(a) where a is Element of A(): a in Y()}
provided
X() = {F(a)` where a is Element of A(): a in Y()};
theorem :: YELLOW_9:1
for R being non empty RelStr, x,y being Element of R holds
y in (uparrow x)` iff not x <= y;
scheme :: YELLOW_9:sch 4
ABC {A() -> TopSpace, F(set) -> set, f() -> Function, P[set]}:
f()"union {F(x) where x is Subset of A(): P[x]} =
union {f()"(F(y)) where y is Subset of A(): P[y]};
theorem :: YELLOW_9:2
for S being 1-sorted, T being non empty 1-sorted, f being Function of S,T
for X being Subset of T holds (f"X)` = f"X`;
theorem :: YELLOW_9:3
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT F = {a` where a is Subset of T: a in F};
theorem :: YELLOW_9:4
for R being non empty RelStr for F being Subset of R holds
uparrow F = union {uparrow x where x is Element of R: x in F} &
downarrow F = union {downarrow x where x is Element of R: x in F};
theorem :: YELLOW_9:5
for R being non empty RelStr
for A being Subset-Family of R, F being Subset of R
st A = {(uparrow x)` where x is Element of R: x in F}
holds Intersect A = (uparrow F)`;
registration
cluster strict complete 1-element for TopLattice;
end;
registration
let S be non empty RelStr,
T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster infs-preserving for Function of S,T;
end;
registration
let S be non empty RelStr,
T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster sups-preserving for Function of S,T;
end;
definition
let R,S be 1-sorted;
assume
the carrier of S c= the carrier of R;
func incl(S,R) -> Function of S,R equals
:: YELLOW_9:def 1
id the carrier of S;
end;
registration
let R be non empty RelStr;
let S be non empty SubRelStr of R;
cluster incl(S,R) -> monotone;
end;
definition
let R be non empty RelStr, X be non empty Subset of R;
func X+id -> strict non empty NetStr over R equals
:: YELLOW_9:def 2
(incl(subrelstr X, R))* (
( subrelstr X)+id);
func X opp+id -> strict non empty NetStr over R equals
:: YELLOW_9:def 3
(incl(subrelstr X, R
) )*((subrelstr X)opp+id);
end;
theorem :: YELLOW_9:6
for R being non empty RelStr, X being non empty Subset of R holds
the carrier of X+id = X & X+id is full SubRelStr of R &
for x being Element of X+id holds X+id.x = x;
theorem :: YELLOW_9:7
for R being non empty RelStr, X being non empty Subset of R holds
the carrier of X opp+id = X & X opp+id is full SubRelStr of R opp &
for x being Element of X opp+id holds X opp+id.x = x;
registration
let R be non empty reflexive RelStr;
let X be non empty Subset of R;
cluster X +id -> reflexive;
cluster X opp+id -> reflexive;
end;
registration
let R be non empty transitive RelStr;
let X be non empty Subset of R;
cluster X +id -> transitive;
cluster X opp+id -> transitive;
end;
registration
let R be non empty reflexive RelStr;
let I be directed Subset of R;
cluster subrelstr I -> directed;
end;
registration
let R be non empty reflexive RelStr;
let I be directed non empty Subset of R;
cluster I+id -> directed;
end;
registration
let R be non empty reflexive RelStr;
let F be filtered non empty Subset of R;
cluster (subrelstr F) opp+id -> directed;
end;
registration
let R be non empty reflexive RelStr;
let F be filtered non empty Subset of R;
cluster F opp+id -> directed;
end;
begin :: Operations on families of open sets
theorem :: YELLOW_9:8
for T being TopSpace st T is empty holds the topology of T = {{}};
theorem :: YELLOW_9:9
for T being 1-element TopSpace holds
the topology of T = bool the carrier of T & for x being Point of T holds
the carrier of T = {x} & the topology of T = {{},{x}};
theorem :: YELLOW_9:10
for T being 1-element TopSpace holds
{the carrier of T} is Basis of T &
{} is prebasis of T & {{}} is prebasis of T;
theorem :: YELLOW_9:11
for X,Y being set, A being Subset-Family of X st A = {Y}
holds FinMeetCl A = {Y,X} & UniCl A = {Y,{}};
theorem :: YELLOW_9:12
for X being set, A,B being Subset-Family of X st A = B \/ {X} or B = A \ { X
} holds Intersect A = Intersect B;
theorem :: YELLOW_9:13
for X being set, A,B being Subset-Family of X st A = B \/ {X} or B = A \ { X
} holds FinMeetCl A = FinMeetCl B;
theorem :: YELLOW_9:14
for X being set, A being Subset-Family of X st X in A
for x being set holds x in FinMeetCl A iff
ex Y being finite non empty Subset-Family of X st Y c= A & x = Intersect Y;
theorem :: YELLOW_9:15
for X being set, A being Subset-Family of X holds UniCl UniCl A = UniCl A;
theorem :: YELLOW_9:16
for X being set, A being empty Subset-Family of X holds UniCl A = {{}};
theorem :: YELLOW_9:17
for X being set, A being empty Subset-Family of X holds FinMeetCl A = {X};
theorem :: YELLOW_9:18
for X being set, A being Subset-Family of X st A = {{},X}
holds UniCl A = A & FinMeetCl A = A;
theorem :: YELLOW_9:19
for X,Y being set, A being Subset-Family of X, B being Subset-Family of Y
holds (A c= B implies UniCl A c= UniCl B) &
(A = B implies UniCl A = UniCl B);
theorem :: YELLOW_9:20
for X,Y being set, A being Subset-Family of X, B being Subset-Family of Y
st A = B & X in A
holds FinMeetCl B = {Y} \/ FinMeetCl A;
theorem :: YELLOW_9:21
for X being set, A being Subset-Family of X holds
UniCl FinMeetCl UniCl A = UniCl FinMeetCl A;
begin :: Bases
theorem :: YELLOW_9:22
for T being TopSpace, K being Subset-Family of T
holds the topology of T = UniCl K iff K is Basis of T;
theorem :: YELLOW_9:23
for T being TopSpace, K being Subset-Family of T
holds K is prebasis of T iff FinMeetCl K is Basis of T;
theorem :: YELLOW_9:24
for T being non empty TopSpace, B being Subset-Family of T
st UniCl B is prebasis of T holds B is prebasis of T;
theorem :: YELLOW_9:25
for T1, T2 being TopSpace, B being Basis of T1
st the carrier of T1 = the carrier of T2 & B is Basis of T2
holds the topology of T1 = the topology of T2;
theorem :: YELLOW_9:26
for T1, T2 being TopSpace, P being prebasis of T1
st the carrier of T1 = the carrier of T2 & P is prebasis of T2
holds the topology of T1 = the topology of T2;
theorem :: YELLOW_9:27
for T being TopSpace, K being Basis of T holds
K is open & K is prebasis of T;
theorem :: YELLOW_9:28
for T being TopSpace, K being prebasis of T holds K is open;
theorem :: YELLOW_9:29
for T being non empty TopSpace, B being prebasis of T holds
B \/ {the carrier of T} is prebasis of T;
theorem :: YELLOW_9:30
for T being TopSpace, B being Basis of T holds
B \/ {the carrier of T} is Basis of T;
theorem :: YELLOW_9:31
for T being TopSpace, B being Basis of T for A being Subset of T holds
A is open iff for p being Point of T st p in A
ex a being Subset of T st a in B & p in a & a c= A;
theorem :: YELLOW_9:32
for T being TopSpace, B being Subset-Family of T st B c= the topology of T &
for A being Subset of T st A is open for p being Point of T st p in A
ex a being Subset of T st a in B & p in a & a c= A holds B is Basis of T;
theorem :: YELLOW_9:33
for S being TopSpace, T being non empty TopSpace, K being Basis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A` is closed;
theorem :: YELLOW_9:34
for S being TopSpace,T being non empty TopSpace, K being Basis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A is open;
theorem :: YELLOW_9:35
for S being TopSpace,T being non empty TopSpace, K being prebasis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A` is closed;
theorem :: YELLOW_9:36
for S being TopSpace,T being non empty TopSpace, K being prebasis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A is open;
theorem :: YELLOW_9:37
for T being non empty TopSpace, x being Point of T, X being Subset of T
for K being Basis of T
st for A being Subset of T st A in K & x in A holds A meets X
holds x in Cl X;
theorem :: YELLOW_9:38
for T being non empty TopSpace, x being Point of T, X being Subset of T
for K being prebasis of T
st for Z being finite Subset-Family of T st Z c= K & x in Intersect Z
holds Intersect Z meets X holds x in Cl X;
theorem :: YELLOW_9:39
for T being non empty TopSpace, K being prebasis of T, x being Point of T
for N being net of T
st for A being Subset of T st A in K & x in A holds N is_eventually_in A
for S being Subset of T st rng netmap(N,T) c= S holds x in Cl S;
begin :: Product topology
theorem :: YELLOW_9:40
for T1,T2 being non empty TopSpace
for B1 being Basis of T1, B2 being Basis of T2 holds
{[:a,b:] where a is Subset of T1, b is Subset of T2: a in B1 & b in B2}
is Basis of [:T1,T2:];
theorem :: YELLOW_9:41
for T1,T2 being non empty TopSpace
for B1 being prebasis of T1, B2 being prebasis of T2 holds
{[:the carrier of T1, b:] where b is Subset of T2: b in B2} \/
{[:a, the carrier of T2:] where a is Subset of T1: a in B1}
is prebasis of [:T1,T2:];
theorem :: YELLOW_9:42
for X1,X2 being set, A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2
st A = {[:a,b:] where a is Subset of X1, b is Subset of X2: a in A1 & b in
A2} holds Intersect A = [:Intersect A1, Intersect A2:];
theorem :: YELLOW_9:43
for T1,T2 being non empty TopSpace
for B1 being prebasis of T1, B2 being prebasis of T2
st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{[:a,b:] where a is Subset of T1, b is Subset of T2: a in B1 & b in B2}
is prebasis of [:T1,T2:];
begin :: Topological augmentations
definition
let R be RelStr;
mode TopAugmentation of R -> TopRelStr means
:: YELLOW_9:def 4
the RelStr of it = the RelStr of R;
end;
notation
let R be RelStr;
let T be TopAugmentation of R;
synonym T is correct for T is TopSpace-like;
end;
registration
let R be RelStr;
cluster correct discrete strict for TopAugmentation of R;
end;
theorem :: YELLOW_9:44
for T being TopRelStr holds T is TopAugmentation of T;
theorem :: YELLOW_9:45
for S being TopRelStr, T being TopAugmentation of S holds
S is TopAugmentation of T;
theorem :: YELLOW_9:46
for R being RelStr, T1 being TopAugmentation of R
for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R;
registration
let R be non empty RelStr;
cluster -> non empty for TopAugmentation of R;
end;
registration
let R be reflexive RelStr;
cluster -> reflexive for TopAugmentation of R;
end;
registration
let R be transitive RelStr;
cluster -> transitive for TopAugmentation of R;
end;
registration
let R be antisymmetric RelStr;
cluster -> antisymmetric for TopAugmentation of R;
end;
registration
let R be complete non empty RelStr;
cluster -> complete for TopAugmentation of R;
end;
theorem :: YELLOW_9:47
for S being up-complete antisymmetric non empty reflexive RelStr,
T being non empty reflexive RelStr st the RelStr of S = the RelStr of T
for A being Subset of S, C being Subset of T st A = C & A is inaccessible
holds C is inaccessible;
theorem :: YELLOW_9:48
for S being non empty reflexive RelStr, T being TopAugmentation of S
st the topology of T = sigma S holds T is correct;
theorem :: YELLOW_9:49
for S being complete LATTICE, T being TopAugmentation of S
st the topology of T = sigma S holds T is Scott;
registration
let R be complete LATTICE;
cluster Scott strict correct for TopAugmentation of R;
end;
theorem :: YELLOW_9:50
for S,T being complete
Scott non empty reflexive transitive antisymmetric TopRelStr
st the RelStr of S = the RelStr of T
for F being Subset of S, G being Subset of T st F = G
holds F is open implies G is open;
theorem :: YELLOW_9:51
for S being complete LATTICE, T being Scott TopAugmentation of S
holds the topology of T = sigma S;
theorem :: YELLOW_9:52
for S,T being complete LATTICE st the RelStr of S = the RelStr of T
holds sigma S = sigma T;
registration
let R be complete LATTICE;
cluster Scott -> correct for TopAugmentation of R;
end;
begin :: Refinements
definition
let T be TopStruct;
mode TopExtension of T -> TopSpace means
:: YELLOW_9:def 5
the carrier of T = the carrier of it &
the topology of T c= the topology of it;
end;
theorem :: YELLOW_9:53
for S being TopStruct ex T being TopExtension of S st
T is strict & the topology of S is prebasis of T;
registration
let T be TopStruct;
cluster strict discrete for TopExtension of T;
end;
definition
let T1,T2 be TopStruct;
mode Refinement of T1,T2 -> TopSpace means
:: YELLOW_9:def 6
the carrier of it = (the carrier of T1) \/ (the carrier of T2) &
(the topology of T1) \/ (the topology of T2) is prebasis of it;
end;
registration
let T1 be non empty TopStruct, T2 be TopStruct;
cluster -> non empty for Refinement of T1,T2;
cluster -> non empty for Refinement of T2,T1;
end;
theorem :: YELLOW_9:54
for T1,T2 being TopStruct, T, T9 being Refinement of T1,T2 holds
the TopStruct of T = the TopStruct of T9;
theorem :: YELLOW_9:55
for T1,T2 being TopStruct, T being Refinement of T1,T2
holds T is Refinement of T2,T1;
theorem :: YELLOW_9:56
for T1,T2 being TopStruct, T being Refinement of T1,T2
for X being Subset-Family of T
st X = (the topology of T1) \/ (the topology of T2)
holds the topology of T = UniCl FinMeetCl X;
theorem :: YELLOW_9:57
for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2
for T being Refinement of T1, T2
holds T is TopExtension of T1 & T is TopExtension of T2;
theorem :: YELLOW_9:58
for T1,T2 being non empty TopSpace, T be Refinement of T1, T2
for B1 being prebasis of T1, B2 being prebasis of T2
holds B1 \/ B2 \/ {the carrier of T1, the carrier of T2} is prebasis of T;
theorem :: YELLOW_9:59
for T1,T2 being non empty TopSpace
for B1 being Basis of T1, B2 being Basis of T2
for T being Refinement of T1, T2
holds B1 \/ B2 \/ INTERSECTION(B1,B2) is Basis of T;
theorem :: YELLOW_9:60
for T1,T2 being non empty TopSpace st the carrier of T1 = the carrier of T2
for T being Refinement of T1, T2
holds INTERSECTION(the topology of T1, the topology of T2) is Basis of T;
theorem :: YELLOW_9:61
for L being non empty RelStr for T1,T2 being correct TopAugmentation of L
for T be Refinement of T1, T2
holds INTERSECTION(the topology of T1, the topology of T2) is Basis of T;