:: On the characteristic and weight of a topological space
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004-2016 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, PRE_TOPC, RLVECT_3, SUBSET_1, TARSKI, SETFAM_1,
RCOMP_1, YELLOW_8, PBOOLE, FUNCT_1, CARD_3, ZFMISC_1, STRUCT_0, RELAT_1,
CARD_1, ORDINAL1, FRECHET, WAYBEL23, FINSET_1, EQREL_1, NATTRA_1, CARD_2,
CANTOR_1, TOPS_1, FINSUB_1, FINSEQ_1, PCOMPS_1, YELLOW_9, TOPGEN_2;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, CARD_1, FINSEQ_1, CARD_3, EQREL_1, ORDINAL1,
FINSET_1, FINSUB_1, CARD_2, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TDLAT_3,
PCOMPS_1, CANTOR_1, FRECHET, YELLOW_8, YELLOW_9, WAYBEL23;
constructors DOMAIN_1, FINSUB_1, CARD_2, TOPS_1, TOPS_2, TDLAT_3, CANTOR_1,
YELLOW_8, YELLOW_9, FRECHET, WAYBEL23, RELSET_1, FINSEQ_2, XTUPLE_0;
registrations SUBSET_1, FINSET_1, CARD_1, EQREL_1, CARD_5, CARD_FIL, STRUCT_0,
PRE_TOPC, TOPS_1, TDLAT_3, YELLOW12, ORDINAL1, COMPTS_1, RELSET_1;
requirements BOOLE, SUBSET, NUMERALS;
begin :: The characteristic of a topological space
reserve a,b,c for set;
::
theorem :: TOPGEN_2:1
for T being non empty TopSpace, B being Basis of T for x being
Element of T holds {U where U is Subset of T: x in U & U in B} is Basis of x;
::
theorem :: TOPGEN_2:2
for T being non empty TopSpace for B being ManySortedSet of T st
for x being Element of T holds B.x is Basis of x holds Union B is Basis of T;
definition
let T be non empty TopStruct;
let x be Element of T;
func Chi(x,T) -> cardinal number means
:: TOPGEN_2:def 1
(ex B being Basis of x st it
= card B) & for B being Basis of x holds it c= card B;
end;
::
theorem :: TOPGEN_2:3
for X being set st for a being set st a in X holds a is cardinal
number holds union X is cardinal number;
definition
let T be non empty TopStruct;
func Chi(T) -> cardinal number means
:: TOPGEN_2:def 2
(for x being Point of T holds
Chi(x,T) c= it) & for M being cardinal number st for x being Point of T holds
Chi(x,T) c= M holds it c= M;
end;
::
theorem :: TOPGEN_2:4
for T being non empty TopStruct holds Chi(T) = union the set of all Chi(x,T)
where x is Point of T;
theorem :: TOPGEN_2:5
for T being non empty TopStruct for x being Point of T holds Chi(
x,T) c= Chi(T);
::
theorem :: TOPGEN_2:6
for T being non empty TopSpace holds T is first-countable iff Chi(T) c= omega
;
begin :: Neighborhood system
definition
let T be non empty TopSpace;
mode Neighborhood_System of T -> ManySortedSet of T means
:: TOPGEN_2:def 3
for x being Element of T holds it.x is Basis of x;
end;
::
definition
let T be non empty TopSpace;
let N be Neighborhood_System of T;
redefine func Union N -> Basis of T;
let x be Point of T;
redefine func N.x -> Basis of x;
end;
::
:: for T being non empty TopSpace
:: for N being Neighborhood_System of T
:: for x being Element of T holds N.x is non empty &
:: for U being set st U in N.x holds x in U
:: by YELLOW_8:21; :: and clusters YELLOW12
::
theorem :: TOPGEN_2:7
for T being non empty TopSpace for x,y being Point of T for B1 being
Basis of x, B2 being Basis of y for U being set st x in U & U in B2 ex V being
open Subset of T st V in B1 & V c= U;
::
theorem :: TOPGEN_2:8
for T being non empty TopSpace for x being Point of T for B being
Basis of x for U1,U2 being set st U1 in B & U2 in B ex V being open Subset of T
st V in B & V c= U1 /\ U2;
::
theorem :: TOPGEN_2:9
for T being non empty TopSpace for A being Subset of T for x being
Element of T holds x in Cl A iff for B being Basis of x for U being set st U in
B holds U meets A;
::
theorem :: TOPGEN_2:10
for T being non empty TopSpace for A being Subset of T for x being
Element of T holds x in Cl A iff ex B being Basis of x st for U being set st U
in B holds U meets A;
registration
let T be TopSpace;
cluster open non empty for Subset-Family of T;
end;
begin :: The weight of a topological space
::
theorem :: TOPGEN_2:11
for T being non empty TopSpace for S being open Subset-Family of
T ex G being open Subset-Family of T st G c= S & union G = union S & card G c=
weight T;
definition
let T be TopStruct;
attr T is finite-weight means
:: TOPGEN_2:def 4
weight T is finite;
end;
notation
let T be TopStruct;
antonym T is infinite-weight for T is finite-weight;
end;
registration
cluster finite -> finite-weight for TopStruct;
cluster infinite-weight -> infinite for TopStruct;
end;
theorem :: TOPGEN_2:12
for X being set holds card SmallestPartition X = card X;
theorem :: TOPGEN_2:13
for T being discrete non empty TopStruct holds SmallestPartition
the carrier of T is Basis of T & for B being Basis of T holds SmallestPartition
the carrier of T c= B;
theorem :: TOPGEN_2:14
for T being discrete non empty TopStruct holds weight T = card
the carrier of T;
registration
cluster infinite-weight for TopSpace;
end;
theorem :: TOPGEN_2:15
for T being finite-weight non empty TopSpace ex B0 being Basis
of T st ex f being Function of the carrier of T, the topology of T st B0 = rng
f & for x being Point of T holds x in f.x & for U being open Subset of T st x
in U holds f.x c= U;
theorem :: TOPGEN_2:16
for T being TopSpace for B0,B being Basis of T for f being
Function of the carrier of T, the topology of T st B0 = rng f & for x being
Point of T holds x in f.x & for U being open Subset of T st x in U holds f.x c=
U holds B0 c= B;
theorem :: TOPGEN_2:17
for T being TopSpace for B0 being Basis of T for f being
Function of the carrier of T, the topology of T st B0 = rng f & for x being
Point of T holds x in f.x & for U being open Subset of T st x in U holds f.x c=
U holds weight T = card B0;
::
theorem :: TOPGEN_2:18
for T being non empty TopSpace for B being Basis of T ex B1 being
Basis of T st B1 c= B & card B1 = weight T;
begin :: Example 1.1.8: Almost discrete topological space with infinity
definition
let X, x0 be set;
func DiscrWithInfin(X,x0) -> strict TopStruct means
:: TOPGEN_2:def 5
the carrier of
it = X & the topology of it = {U where U is Subset of X: not x0 in U} \/ {F`
where F is Subset of X: F is finite};
end;
registration
let X,x0 be set;
cluster DiscrWithInfin(X,x0) -> TopSpace-like;
end;
registration
let X be non empty set, x0 be set;
cluster DiscrWithInfin(X,x0) -> non empty;
end;
theorem :: TOPGEN_2:19
for X,x0 being set, A being Subset of DiscrWithInfin(X,x0) holds
A is open iff not x0 in A or A` is finite;
theorem :: TOPGEN_2:20
for X,x0 being set, A being Subset of DiscrWithInfin(X,x0) holds
A is closed iff (x0 in X implies x0 in A) or A is finite;
theorem :: TOPGEN_2:21
for X,x0,x being set st x in X holds {x} is closed Subset of
DiscrWithInfin(X,x0);
theorem :: TOPGEN_2:22
for X,x0,x being set st x in X & x <> x0 holds {x} is open
Subset of DiscrWithInfin(X,x0);
theorem :: TOPGEN_2:23
for X,x0 being set st X is infinite for U being Subset of
DiscrWithInfin(X,x0) st U = {x0} holds U is not open;
theorem :: TOPGEN_2:24
for X,x0 being set for A being Subset of DiscrWithInfin(X,x0) st
A is finite holds Cl A = A;
theorem :: TOPGEN_2:25
for T being non empty TopSpace for A being Subset of T st A is
not closed for a being Point of T st A \/ {a} is closed holds Cl A = A \/ {a}
;
theorem :: TOPGEN_2:26
for X,x0 being set st x0 in X for A being Subset of
DiscrWithInfin(X,x0) st A is infinite holds Cl A = A \/ {x0};
theorem :: TOPGEN_2:27
for X,x0 being set for A being Subset of DiscrWithInfin(X,x0) st A` is
finite holds Int A = A;
theorem :: TOPGEN_2:28
for X,x0 being set st x0 in X for A being Subset of DiscrWithInfin(X,
x0) st A` is infinite holds Int A = A \ {x0};
theorem :: TOPGEN_2:29
for X, x0 being set holds ex B0 being Basis of DiscrWithInfin(X,
x0) st B0 = ((SmallestPartition X) \ {{x0}}) \/ {F` where F is Subset of X: F
is finite};
theorem :: TOPGEN_2:30
for X being infinite set holds card Fin X = card X;
theorem :: TOPGEN_2:31
for X being infinite set holds card {F` where F is Subset of X:
F is finite} = card X;
theorem :: TOPGEN_2:32
for X being infinite set, x0 being set for B0 being Basis of
DiscrWithInfin(X,x0) st B0 = ((SmallestPartition X) \ {{x0}}) \/ {F` where F is
Subset of X: F is finite} holds card B0 = card X;
theorem :: TOPGEN_2:33
for X being infinite set, x0 being set for B being Basis of
DiscrWithInfin(X,x0) holds card X c= card B;
theorem :: TOPGEN_2:34
for X being infinite set, x0 being set holds weight DiscrWithInfin(X,
x0) = card X;
theorem :: TOPGEN_2:35
for X being non empty set, x0 being set holds ex B0 being prebasis of
DiscrWithInfin(X,x0) st B0 = ((SmallestPartition X) \ {{x0}}) \/ the set of
all {x}` where x
is Element of X;
begin :: Exercises
::
theorem :: TOPGEN_2:36
for T being TopSpace, F being Subset-Family of T for I being non empty
Subset-Family of F st for G being set st G in I holds F\G is finite holds Cl
union F = union clf F \/ meet {Cl union G where G is Subset-Family of T: G in I
};
::
theorem :: TOPGEN_2:37
for T being TopSpace, F being Subset-Family of T holds Cl union F =
union clf F \/ meet {Cl union G where G is Subset-Family of T: G c= F & F\G is
finite};
::
theorem :: TOPGEN_2:38
for X being set, O being Subset-Family of bool X st for o being
Subset-Family of X st o in O holds TopStruct(#X,o#) is TopSpace ex B being
Subset-Family of X st B = Intersect O & TopStruct(#X,B#) is TopSpace & (for o
being Subset-Family of X st o in O holds TopStruct(#X,o#) is TopExtension of
TopStruct(#X,B#)) & for T being TopSpace st the carrier of T = X & for o being
Subset-Family of X st o in O holds TopStruct(#X,o#) is TopExtension of T holds
TopStruct(#X,B#) is TopExtension of T;
::
theorem :: TOPGEN_2:39
for X being set, O being Subset-Family of bool X ex B being
Subset-Family of X st B = UniCl FinMeetCl union O & TopStruct(#X,B#) is
TopSpace & (for o being Subset-Family of X st o in O holds TopStruct(#X,B#) is
TopExtension of TopStruct(#X,o#)) & for T being TopSpace st the carrier of T =
X & for o being Subset-Family of X st o in O holds T is TopExtension of
TopStruct(#X,o#) holds T is TopExtension of TopStruct(#X,B#);