:: On the characteristic and weight of a topological space
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004-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, 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;
definitions TARSKI, XBOOLE_0, FUNCT_1, CARD_3, STRUCT_0, PRE_TOPC, FRECHET,
YELLOW_8, YELLOW_9;
equalities XBOOLE_0, CARD_3, STRUCT_0, SUBSET_1;
expansions TARSKI, CARD_3, PRE_TOPC;
theorems XBOOLE_1, ZFMISC_1, SETFAM_1, CANTOR_1, CARD_5, YELLOW_8, YELLOW_9,
TOPS_1, CARD_1, CARD_4, CARD_LAR, XBOOLE_0, TSEP_1, PRE_TOPC, TARSKI,
TOPS_2, FUNCT_1, CARD_3, FINSET_1, TDLAT_3, CARD_2, EQREL_1, FUNCT_2,
WELLORD2, WAYBEL23, SUBSET_1, FINSEQ_1, FINSUB_1, WAYBEL19, PCOMPS_1,
MSSUBFAM, ENUMSET1, PARTFUN1;
schemes ORDINAL1, PBOOLE, FUNCT_1, FUNCT_2;
begin :: The characteristic of a topological space
reserve a,b,c for set;
::<DESC name="baza w punkcie a baza" monograph="topology"/>
theorem Th1:
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
proof
let T be non empty TopSpace;
let B be Basis of T;
let x be Element of T;
set Bx = {U where U is Subset of T: x in U & U in B};
A1: Bx c= B
proof
let a be object;
assume a in Bx;
then ex U being Subset of T st a = U & x in U & U in B;
hence thesis;
end;
then reconsider Bx as Subset-Family of T by XBOOLE_1:1;
Bx is Basis of x
proof
B c= the topology of T by TOPS_2:64;
then Bx c= the topology of T by A1;
then
A2: Bx is open by TOPS_2:64;
Bx is x-quasi_basis
proof
now
let a;
assume a in Bx;
then ex U being Subset of T st a = U & x in U & U in B;
hence x in a;
end;
hence x in Intersect Bx by SETFAM_1:43;
let S be Subset of T such that
A3: S is open and
A4: x in S;
consider V being Subset of T such that
A5: V in B and
A6: x in V and
A7: V c= S by A3,A4,YELLOW_9:31;
V in Bx by A5,A6;
hence thesis by A7;
end;
hence thesis by A2;
end;
hence thesis;
end;
::<DESC name="baza w punkcie a baza" monograph="topology"/>
theorem Th2:
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
proof
let T be non empty TopSpace;
let B be ManySortedSet of T;
assume
A1: for x being Element of T holds B.x is Basis of x;
Union B c= bool the carrier of T
proof
let a be object;
assume a in Union B;
then consider b being object such that
A2: b in dom B and
A3: a in B.b by CARD_5:2;
reconsider b as Point of T by A2;
B.b is Basis of b by A1;
hence thesis by A3;
end;
then reconsider W = Union B as Subset-Family of T;
A4: dom B = the carrier of T by PARTFUN1:def 2;
A5: now
let A be Subset of T such that
A6: A is open;
let p be Point of T such that
A7: p in A;
A8: B.p is Basis of p by A1;
then consider a being Subset of T such that
A9: a in B.p and
A10: a c= A by A6,A7,YELLOW_8:def 1;
take a;
thus a in W by A4,A9,CARD_5:2;
thus p in a by A8,A9,YELLOW_8:12;
thus a c= A by A10;
end;
W c= the topology of T
proof
let a be object;
assume a in W;
then consider b being object such that
A11: b in dom B and
A12: a in B.b by CARD_5:2;
reconsider b as Point of T by A11;
B.b is Basis of b by A1;
then B.b c= the topology of T by TOPS_2:64;
hence thesis by A12;
end;
hence thesis by A5,YELLOW_9:32;
end;
definition
let T be non empty TopStruct;
let x be Element of T;
func Chi(x,T) -> cardinal number means
: Def1:
(ex B being Basis of x st it
= card B) & for B being Basis of x holds it c= card B;
existence
proof
set B0 = the Basis of x;
defpred P[Ordinal] means ex B being Basis of x st $1 = card B;
card B0 is ordinal;
then
A1: ex A being Ordinal st P[A];
consider A being Ordinal such that
A2: P[A] and
A3: for B being Ordinal st P[B] holds A c= B from ORDINAL1:sch
1(A1);
consider B1 being Basis of x such that
A4: A = card B1 by A2;
take card B1;
thus thesis by A3,A4;
end;
uniqueness
proof
let M1, M2 be cardinal number;
assume that
A5: ex B being Basis of x st M1 = card B and
A6: for B being Basis of x holds M1 c= card B and
A7: ex B being Basis of x st M2 = card B and
A8: for B being Basis of x holds M2 c= card B;
thus M1 c= M2 & M2 c= M1 by A5,A6,A7,A8;
end;
end;
::<DESC name="charakter punktu" monograph="topology"/>
theorem Th3:
for X being set st for a being set st a in X holds a is cardinal
number holds union X is cardinal number
proof
let X be set such that
A1: for a being set st a in X holds a is cardinal number;
now
let a;
assume
A2: a in X;
then a is cardinal number by A1;
hence ex b being set st b in X & a c= b & b is cardinal set by A2;
end;
hence thesis by CARD_LAR:32;
end;
Lm1: now
let T be non empty TopStruct;
set X = the set of all Chi(x,T) where x is Point of T;
now
let a;
assume a in X;
then ex x being Point of T st a = Chi(x,T);
hence a is cardinal number;
end;
hence union X is cardinal number by Th3;
let m be cardinal number such that
A1: m = union X;
hereby
let x be Point of T;
Chi(x,T) in X;
hence Chi(x,T) c= m by A1,ZFMISC_1:74;
end;
let M be cardinal number such that
A2: for x being Point of T holds Chi(x,T) c= M;
now
let a;
assume a in X;
then ex x being Point of T st a = Chi(x,T);
hence a c= M by A2;
end;
hence m c= M by A1,ZFMISC_1:76;
end;
definition
let T be non empty TopStruct;
func Chi(T) -> cardinal number means
: Def2:
(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;
existence
proof
set X = the set of all Chi(x,T) where x is Point of T;
reconsider m = union X as cardinal number by Lm1;
take m;
thus thesis by Lm1;
end;
uniqueness
proof
let M1, M2 be cardinal number;
assume that
A1: for x being Point of T holds Chi(x,T) c= M1 and
A2: for M being cardinal number st for x being Point of T holds Chi(x,
T ) c= M holds M1 c= M and
A3: for x being Point of T holds Chi(x,T) c= M2 and
A4: for M being cardinal number st for x being Point of T holds Chi(x,
T) c= M holds M2 c= M;
thus M1 c= M2 & M2 c= M1 by A1,A2,A3,A4;
end;
end;
::<DESC name="charakter przestrzeni" monograph="topology"/>
theorem Th4:
for T being non empty TopStruct holds Chi(T) = union the set of all Chi(x,T)
where x is Point of T
proof
let T be non empty TopStruct;
set X = the set of all Chi(x,T) where x is Point of T;
reconsider m = union X as cardinal number by Lm1;
A1: for M being cardinal number st for x being Point of T holds Chi(x,T) c=
M holds m c= M by Lm1;
for x being Point of T holds Chi(x,T) c= m by Lm1;
hence thesis by A1,Def2;
end;
theorem Th5:
for T being non empty TopStruct for x being Point of T holds Chi(
x,T) c= Chi(T)
proof
let T be non empty TopStruct;
set X = the set of all Chi(x,T) where x is Point of T;
let x be Point of T;
A1: Chi(x,T) in X;
Chi(T) = union X by Th4;
hence thesis by A1,ZFMISC_1:74;
end;
::<DESC name="pierwszy aksjomat przeliczalno/sci" monograph="topology"/>
theorem
for T being non empty TopSpace holds T is first-countable iff Chi(T) c= omega
proof
let T be non empty TopSpace;
set X = the set of all Chi(x,T) where x is Point of T;
A1: Chi(T) = union X by Th4;
thus T is first-countable implies Chi(T) c= omega
proof
assume
A2: for x be Point of T ex B be Basis of x st B is countable;
now
let a;
assume a in X;
then consider x being Point of T such that
A3: a = Chi(x,T);
consider B being Basis of x such that
A4: B is countable by A2;
A5: card B c= omega by A4;
Chi(x,T) c= card B by Def1;
hence a c= omega by A3,A5;
end;
hence thesis by A1,ZFMISC_1:76;
end;
assume
A6: Chi(T) c= omega;
let x be Point of T;
consider B being Basis of x such that
A7: Chi(x,T) = card B by Def1;
take B;
Chi(x,T) c= Chi(T) by Th5;
hence card B c= omega by A6,A7;
end;
begin :: Neighborhood system
definition
let T be non empty TopSpace;
mode Neighborhood_System of T -> ManySortedSet of T means
: Def3:
for x being Element of T holds it.x is Basis of x;
existence
proof
set B = the Basis of T;
deffunc F(Point of T) = {U where U is Subset of T: $1 in U & U in B};
consider F being ManySortedSet of T such that
A1: for x being Point of T holds F.x = F(x) from PBOOLE:sch 5;
take F;
let x be Point of T;
F.x = F(x) by A1;
hence thesis by Th1;
end;
end;
::<DESC name="uk/lad otocze/n" monograph="topology"/>
definition
let T be non empty TopSpace;
let N be Neighborhood_System of T;
redefine func Union N -> Basis of T; :: redefines Union (CARD_3, definition)
coherence
proof
for x being Point of T holds N.x is Basis of x by Def3;
hence thesis by Th2;
end;
let x be Point of T;
redefine func N.x -> Basis of x; :: redefines . (FUNCT_1, definition)
coherence by Def3;
end;
::<DESC name="uk/lad otocze/n: (BP1)" monograph="topology"/>
:: 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
::<DESC name="uk/lad otocze/n: (BP2)" monograph="topology"/>
theorem
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
proof
let T be non empty TopSpace;
let x,y be Point of T;
let B1 be Basis of x;
let B2 be Basis of y;
let U be set;
assume that
A1: x in U and
A2: U in B2;
U is open Subset of T by A2,YELLOW_8:12;
then consider V being Subset of T such that
A3: V in B1 and
A4: V c= U by A1,YELLOW_8:13;
V is open by A3,YELLOW_8:12;
hence thesis by A3,A4;
end;
::<DESC name="uk/lad otocze/n: (BP3)" monograph="topology"/>
theorem
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
proof
let T be non empty TopSpace;
let x be Point of T;
let B be Basis of x;
let U1,U2 be set;
assume that
A1: U1 in B and
A2: U2 in B;
reconsider U1, U2 as open Subset of T by A1,A2,YELLOW_8:12;
A3: x in U2 by A2,YELLOW_8:12;
x in U1 by A1,YELLOW_8:12;
then x in U1/\U2 by A3,XBOOLE_0:def 4;
then consider V being Subset of T such that
A4: V in B and
A5: V c= U1/\U2 by YELLOW_8:13;
V is open by A4,YELLOW_8:12;
hence thesis by A4,A5;
end;
Lm2: now
let T be non empty TopSpace;
let A be Subset of T;
let x be Element of T such that
A1: x in Cl A;
let B be Basis of x, U be set;
assume
A2: U in B;
then x in U by YELLOW_8:12;
then U meets Cl A by A1,XBOOLE_0:3;
hence U meets A by A2,TSEP_1:36,YELLOW_8:12;
end;
Lm3: now
let T be non empty TopSpace;
let A be Subset of T;
let x be Element of T;
given B being Basis of x such that
A1: for U being set st U in B holds U meets A;
now
let U be Subset of T;
assume that
A2: U is open and
A3: x in U;
ex V being Subset of T st V in B & V c= U by A2,A3,YELLOW_8:def 1;
hence A meets U by A1,XBOOLE_1:63;
end;
hence x in Cl A by PRE_TOPC:def 7;
end;
::<DESC name="1.1.1. Twierdzenie: Cl a baza w punkcie" monograph="topology"/>
theorem
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
proof
let T be non empty TopSpace;
let A be Subset of T;
let x be Element of T;
set B = the Basis of x;
thus x in Cl A implies for B being Basis of x for U being set st U in B
holds U meets A by Lm2;
assume for B being Basis of x for U being set st U in B holds U meets A;
then for U being set st U in B holds U meets A;
hence thesis by Lm3;
end;
::<DESC name="1.1.1. Twierdzenie: Cl a baza w punkcie" monograph="topology"/>
theorem
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
proof
let T be non empty TopSpace;
let A be Subset of T;
let x be Element of T;
set B = the Basis of x;
x in Cl A implies for U being set st U in B holds U meets A by Lm2;
hence x in Cl A implies ex B being Basis of x st for U being set st U in B
holds U meets A;
thus thesis by Lm3;
end;
registration
let T be TopSpace;
cluster open non empty for Subset-Family of T;
existence
proof
take the topology of T;
thus thesis;
end;
end;
begin :: The weight of a topological space
::<DESC name="1.1.14. Twierdzenie: istnienie podrodziny mocy niewi/ekszej od wagi przestrzeni i o unii r/ownej" monograph="topology"/>
theorem Th11:
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
proof
defpred P[object,object] means
ex A,B being set st A = $1 & B = $2 & A c= B;
let T be non empty TopSpace;
let S be open Subset-Family of T;
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:74;
set B1 = {W where W is Subset of T: W in B & ex U being set st U in S & W c=
U};
B1 c= B
proof
let a be object;
assume a in B1;
then
ex W being Subset of T st a = W & W in B & ex U being set st U in S &
W c= U;
hence thesis;
end;
then
A2: card B1 c= card B by CARD_1:11;
A3: now
let a be object;
assume a in B1;
then
ex W being Subset of T st a = W & W in B & ex U being set st U in S &
W c= U;
hence ex b being object st b in S & P[a,b];
end;
consider f being Function such that
A4: dom f = B1 & rng f c= S and
A5: for a being object st a in B1 holds P[a,f.a] from FUNCT_1:sch 6(A3);
set G = rng f;
reconsider G as open Subset-Family of T by A4,TOPS_2:11,XBOOLE_1:1;
take G;
thus G c= S & union G c= union S by A4,ZFMISC_1:77;
thus union S c= union G
proof
let a be object;
assume a in union S;
then consider b such that
A6: a in b and
A7: b in S by TARSKI:def 4;
reconsider b as open Subset of T by A7,TOPS_2:def 1;
reconsider a as Point of T by A6,A7;
consider W0 being Subset of T such that
A8: W0 in B and
A9: a in W0 and
A10: W0 c= b by A6,YELLOW_9:31;
A11: W0 in B1 by A7,A8,A10;
then f.W0 in G by A4,FUNCT_1:def 3;
then
A12: f.W0 c= union G by ZFMISC_1:74;
P[W0,f.W0] by A5,A11;
then W0 c= f.W0;
then a in f.W0 by A9;
hence thesis by A12;
end;
card G c= card B1 by A4,CARD_1:12;
hence thesis by A1,A2;
end;
definition
let T be TopStruct;
attr T is finite-weight means
: Def4:
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;
coherence
proof
let T be TopStruct;
assume
A1: the carrier of T is finite;
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence weight T is finite by A1;
end;
cluster infinite-weight -> infinite for TopStruct;
coherence;
end;
theorem Th12:
for X being set holds card SmallestPartition X = card X
proof
let X be set;
set A = SmallestPartition X;
per cases;
suppose
X = {};
hence thesis;
end;
suppose
X <> {};
then reconsider X as non empty set;
deffunc F(object) = {$1};
A1: A = the set of all {x} where x is Element of X by EQREL_1:37;
then
A2: for a being object st a in X holds F(a) in A;
consider f being Function of X,A such that
A3: for a being object st a in X holds f.a = F(a) from FUNCT_2:sch 2(A2);
A4: rng f = A
proof
thus rng f c= A;
let a be object;
assume a in A;
then consider b being Element of X such that
A5: a = {b} by A1;
f.b = a by A3,A5;
hence thesis by FUNCT_2:4;
end;
A6: f is one-to-one
proof
let a,b be object;
assume that
A7: a in dom f and
A8: b in dom f;
assume f.a = f.b;
then {a} = f.b by A3,A7
.= {b} by A3,A8;
hence thesis by ZFMISC_1:3;
end;
dom f = X by FUNCT_2:def 1;
then X,A are_equipotent by A4,A6,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
end;
theorem Th13:
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
proof
let T be discrete non empty TopStruct;
set B0 = SmallestPartition the carrier of T;
A1: B0 c= the topology of T
proof
let a be object;
assume a in B0;
then reconsider a as Subset of T;
a is open by TDLAT_3:15;
hence thesis;
end;
A2: B0 = the set of all {a} where a is Element of T by EQREL_1:37;
now
let A be Subset of T such that
A is open;
let p be Point of T such that
A3: p in A;
reconsider a = {p} as Subset of T;
take a;
thus a in B0 by A2;
thus p in a by TARSKI:def 1;
thus a c= A by A3,ZFMISC_1:31;
end;
hence
A4: B0 is Basis of T by A1,YELLOW_9:32;
let B be Basis of T;
let a be object;
assume
A5: a in B0;
then consider b being Element of T such that
A6: a = {b} by A2;
reconsider a as Subset of T by A5;
A7: b in a by A6,TARSKI:def 1;
a is open by A4,A5,YELLOW_8:10;
then consider U being Subset of T such that
A8: U in B and
A9: b in U and
A10: U c= a by A7,YELLOW_9:31;
a c= U by A6,A9,ZFMISC_1:31;
hence thesis by A8,A10,XBOOLE_0:def 10;
end;
theorem Th14:
for T being discrete non empty TopStruct holds weight T = card
the carrier of T
proof
let T be discrete non empty TopStruct;
set M = the set of all card C where C is Basis of T;
reconsider B0 = SmallestPartition the carrier of T as Basis of T by Th13;
A1: card B0 in M;
A2: card B0 = card the carrier of T by Th12;
weight T = meet M by WAYBEL23:def 5;
hence weight T c= card the carrier of T by A2,A1,SETFAM_1:3;
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence card the carrier of T c= weight T by A2,Th13,CARD_1:11;
end;
registration
cluster infinite-weight for TopSpace;
existence
proof
set A = the infinite set;
reconsider O = bool A as Subset-Family of A;
reconsider T = TopStruct(#A, O#) as discrete non empty TopStruct by
TDLAT_3:def 1;
take T;
weight T = card the carrier of T by Th14;
hence weight T is infinite;
end;
end;
Lm4: for T being infinite-weight TopSpace for B being Basis of T ex B1 being
Basis of T st B1 c= B & card B1 = weight T
proof
let T be infinite-weight TopSpace;
let B be Basis of T;
consider B0 being Basis of T such that
A1: card B0 = weight T by WAYBEL23:74;
defpred P[object,object] means
ex A being set st A = $2 & union A = $1 & card A c= weight T;
A2: now
let a be object;
reconsider aa = a as set by TARSKI:1;
set Sa = {U where U is Subset of T: U in B & U c= aa};
A3: Sa c= B
proof
let b be object;
assume b in Sa;
then ex U being Subset of T st b = U & U in B & U c= aa;
hence thesis;
end;
assume a in B0;
then reconsider W = a as open Subset of T by YELLOW_8:10;
A4: union Sa = W by YELLOW_8:9;
reconsider Sa as open Subset-Family of T by A3,TOPS_2:11,XBOOLE_1:1;
consider G being open Subset-Family of T such that
A5: G c= Sa and
A6: union G = union Sa and
A7: card G c= weight T by Th11;
reconsider b = G as object;
take b;
G c= B by A3,A5;
hence b in bool B;
thus P[a,b] by A4,A6,A7;
end;
consider f being Function such that
A8: dom f = B0 & rng f c= bool B and
A9: for a being object st a in B0 holds P[a,f.a] from FUNCT_1:sch 6(A2);
A10: Union f c= union bool B by A8,ZFMISC_1:77;
then
A11: Union f c= B by ZFMISC_1:81;
then reconsider B1 = Union f as Subset-Family of T by XBOOLE_1:1;
now
B c= the topology of T by TOPS_2:64;
hence B1 c= the topology of T by A11;
let A be Subset of T such that
A12: A is open;
let p be Point of T;
assume p in A;
then consider U being Subset of T such that
A13: U in B0 and
A14: p in U and
A15: U c= A by A12,YELLOW_9:31;
A16: P[U,f.U] by A9,A13;
then consider a such that
A17: p in a and
A18: a in f.U by A14,TARSKI:def 4;
A19: a c= U by A16,A18,ZFMISC_1:74;
a in B1 by A8,A13,A18,CARD_5:2;
hence ex a being Subset of T st a in B1 & p in a & a c= A by A15,A17,A19,
XBOOLE_1:1;
end;
then reconsider B1 as Basis of T by YELLOW_9:32;
now
thus card rng f c= weight T by A1,A8,CARD_1:12;
let a;
assume a in rng f;
then consider b being object such that
A20: b in dom f & a = f.b by FUNCT_1:def 3;
P[b,f.b] by A8,A9,A20;
hence card a c= weight T by A20;
end;
then
A21: card B1 c= (weight T)*`(weight T) by CARD_2:87;
take B1;
thus B1 c= B by A10,ZFMISC_1:81;
weight T is infinite by Def4;
hence card B1 c= weight T by A21,CARD_4:15;
thus thesis by WAYBEL23:73;
end;
theorem Th15:
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
proof
let T be finite-weight non empty TopSpace;
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:74;
deffunc F(object) = meet {U where U is Subset of T: $1 in U & U in B};
A2: B is finite by A1,Def4;
A3: now
B c= the topology of T by TOPS_2:64;
then FinMeetCl B c= FinMeetCl the topology of T by CANTOR_1:14;
then
A4: FinMeetCl B c= the topology of T by CANTOR_1:5;
let a be object;
assume a in the carrier of T;
then reconsider x = a as Point of T;
set S = {U where U is Subset of T: x in U & U in B};
consider U being Subset of T such that
A5: U in B and
A6: x in U and
U c= [#]T by YELLOW_9:31;
A7: S c= B
proof
let a be object;
assume a in S;
then ex U being Subset of T st a = U & x in U & U in B;
hence thesis;
end;
then reconsider S as Subset-Family of T by XBOOLE_1:1;
Intersect S in FinMeetCl B by A2,A7,CANTOR_1:def 3;
then
A8: Intersect S in the topology of T by A4;
U in S by A5,A6;
hence F(a) in the topology of T by A8,SETFAM_1:def 9;
end;
consider f being Function of the carrier of T, the topology of T such that
A9: for a being object st a in the carrier of T holds f.a = F(a)
from FUNCT_2:sch 2(
A3);
set B0 = rng f;
reconsider B0 as Subset-Family of T by XBOOLE_1:1;
A10: now
let a;
assume a in the carrier of T;
then reconsider x = a as Point of T;
set S = {U where U is Subset of T: x in U & U in B};
consider U being Subset of T such that
A11: U in B and
A12: x in U and
U c= [#]T by YELLOW_9:31;
A13: now
let b;
assume b in S;
then ex U being Subset of T st b = U & a in U & U in B;
hence a in b;
end;
A14: f.a = meet S by A9;
U in S by A11,A12;
hence a in f.a by A14,A13,SETFAM_1:def 1;
end;
A15: now
let x be Point of T, V be Subset of T;
set S = {U where U is Subset of T: x in U & U in B};
assume that
A16: x in V and
A17: V is open;
consider U being Subset of T such that
A18: U in B and
A19: x in U and
A20: U c= V by A16,A17,YELLOW_9:31;
A21: f.x = meet S by A9;
U in S by A18,A19;
then f.x c= U by A21,SETFAM_1:3;
hence f.x c= V by A20;
end;
now
let A be Subset of T;
assume
A22: A is open;
let p be Point of T;
assume
A23: p in A;
f.p in the topology of T;
then reconsider a = f.p as Subset of T;
take a;
thus a in B0 by FUNCT_2:4;
thus p in a by A10;
thus a c= A by A15,A22,A23;
end;
then reconsider B0 as Basis of T by YELLOW_9:32;
take B0,f;
thus B0 = rng f;
let x be Point of T;
thus thesis by A10,A15;
end;
theorem Th16:
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
proof
let T be TopSpace;
let B0,B be Basis of T;
let f be Function of the carrier of T, the topology of T;
assume
A1: B0 = rng f;
assume
A2: 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;
let a be object;
assume
A3: a in B0;
then reconsider V = a as Subset of T;
consider b being object such that
A4: b in dom f and
A5: a = f.b by A1,A3,FUNCT_1:def 3;
A6: V is open by A3,YELLOW_8:10;
reconsider b as Element of T by A4;
b in V by A2,A5;
then consider U being Subset of T such that
A7: U in B and
A8: b in U and
A9: U c= V by A6,YELLOW_9:31;
U is open by A7,YELLOW_8:10;
then f.b c= U by A2,A8;
hence thesis by A7,A9,XBOOLE_0:def 10,A5;
end;
theorem Th17:
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
proof
let T be TopSpace;
let B0 be Basis of T;
let f be Function of the carrier of T, the topology of T such that
A1: B0 = rng f and
A2: 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;
set M = the set of all card C where C is Basis of T;
A3: card B0 in M;
weight T = meet M by WAYBEL23:def 5;
hence weight T c= card B0 by A3,SETFAM_1:3;
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence thesis by A1,A2,Th16,CARD_1:11;
end;
Lm5: for T being finite-weight non empty TopSpace for B being Basis of T ex B1
being Basis of T st B1 c= B & card B1 = weight T
proof
let T be finite-weight non empty TopSpace;
let B be Basis of T;
consider B0 being Basis of T, f being Function of the carrier of T, the
topology of T such that
A1: B0 = rng f and
A2: 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 by Th15;
take B0;
thus B0 c= B by A1,A2,Th16;
thus card B0 c= weight T by A1,A2,Th17;
thus thesis by WAYBEL23:73;
end;
::<DESC name="1.1.15. Twierdzenie: o istnieniu bazy bed/acej podrodzin/a bazy i maj/acej moc r/own/a wadze przestrzeni" monograph="topology"/>
theorem
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
proof
let T be non empty TopSpace, B be Basis of T;
T is finite-weight or T is infinite-weight;
hence thesis by Lm4,Lm5;
end;
begin :: Example 1.1.8: Almost discrete topological space with infinity
definition
let X, x0 be set;
func DiscrWithInfin(X,x0) -> strict TopStruct means
: Def5:
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};
uniqueness;
existence
proof
set O1 = {U where U is Subset of X: not x0 in U}, O2 = {F` where F is
Subset of X: F is finite}, O = O1 \/ O2;
O c= bool X
proof
let a be object;
assume a in O;
then a in O1 or a in O2 by XBOOLE_0:def 3;
then
(ex U being Subset of X st a = U & not x0 in U) or ex F being Subset
of X st a = F` & F is finite;
hence thesis;
end;
then reconsider O as Subset-Family of X;
take TopStruct(#X,O#);
thus thesis;
end;
end;
registration
let X,x0 be set;
cluster DiscrWithInfin(X,x0) -> TopSpace-like;
coherence
proof
set O1 = {U where U is Subset of X: not x0 in U}, O2 = {F` where F is
Subset of X: F is finite}, O = O1 \/ O2;
set T = DiscrWithInfin(X,x0);
A1: the carrier of T = X by Def5;
A2: the topology of T = O by Def5;
({}X)` = X;
then X in O2;
hence the carrier of T in the topology of T by A1,A2,XBOOLE_0:def 3;
hereby
let a be Subset-Family of T such that
A3: a c= the topology of T;
per cases;
suppose
not a c= O1;
then consider b being object such that
A4: b in a and
A5: not b in O1;
reconsider bb=b as set by TARSKI:1;
b in O2 by A2,A3,A4,A5,XBOOLE_0:def 3;
then
A6: ex F being Subset of X st b = F` & F is finite;
A7: (union a)`` = union a;
bb c= union a by A4,ZFMISC_1:74;
then (union a)` is finite by A1,A6,FINSET_1:1,SUBSET_1:17;
then union a in O2 by A1,A7;
hence union a in the topology of T by A2,XBOOLE_0:def 3;
end;
suppose
A8: a c= O1;
now
assume x0 in union a;
then consider b such that
A9: x0 in b and
A10: b in a by TARSKI:def 4;
b in O1 by A8,A10;
then ex U being Subset of X st b = U & not x0 in U;
hence contradiction by A9;
end;
then union a in O1 by A1;
hence union a in the topology of T by A2,XBOOLE_0:def 3;
end;
end;
let a,b be Subset of T;
assume that
A11: a in the topology of T and
A12: b in the topology of T;
per cases by A2,A11,A12,XBOOLE_0:def 3;
suppose
A13: a in O2 & b in O2;
then consider F2 being Subset of X such that
A14: b = F2` and
A15: F2 is finite;
consider F1 being Subset of X such that
A16: a = F1` and
A17: F1 is finite by A13;
a/\b = (F1\/F2)` by A16,A14,XBOOLE_1:53;
then a/\b in O2 by A17,A15;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose
a in O1 or b in O1;
then (ex U being Subset of X st a = U & not x0 in U) or ex U being
Subset of X st b = U & not x0 in U;
then not x0 in a/\b by XBOOLE_0:def 4;
then a/\b in O1 by A1;
hence thesis by A2,XBOOLE_0:def 3;
end;
end;
end;
registration
let X be non empty set, x0 be set;
cluster DiscrWithInfin(X,x0) -> non empty;
coherence by Def5;
end;
theorem Th19:
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
proof
let X,x0 be set;
set T = DiscrWithInfin(X,x0);
set O1 = {U where U is Subset of X: not x0 in U};
set O2 = {F` where F is Subset of X: F is finite};
let A be Subset of T;
A1: the topology of T = O1 \/ O2 by Def5;
A2: the carrier of T = X by Def5;
thus A is open implies not x0 in A or A` is finite
proof
assume A in the topology of T;
then A in O1 or A in O2 by A1,XBOOLE_0:def 3;
then (ex U being Subset of X st A = U & not x0 in U) or ex F being Subset
of X st A = F` & F is finite;
hence thesis by A2;
end;
assume not x0 in A or A` is finite;
then A in O1 or A`` in O2 by A2;
hence A in the topology of T by A1,XBOOLE_0:def 3;
end;
theorem Th20:
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
proof
let X,x0 be set;
set T = DiscrWithInfin(X,x0);
let A be Subset of DiscrWithInfin(X,x0);
A1: A is closed iff not x0 in A` or A`` is finite by Th19;
the carrier of T = X by Def5;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem
for X,x0,x being set st x in X holds {x} is closed Subset of
DiscrWithInfin(X,x0)
proof
let X,x0,x be set;
set T = DiscrWithInfin(X,x0);
the carrier of T = X by Def5;
hence thesis by Th20,ZFMISC_1:31;
end;
theorem Th22:
for X,x0,x being set st x in X & x <> x0 holds {x} is open
Subset of DiscrWithInfin(X,x0)
proof
let X,x0,x be set;
set T = DiscrWithInfin(X,x0);
assume that
A1: x in X and
A2: x <> x0;
A3: the carrier of T = X by Def5;
not x0 in {x} by A2,TARSKI:def 1;
hence thesis by A3,A1,Th19,ZFMISC_1:31;
end;
theorem
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
proof
let X,x0 be set;
set T = DiscrWithInfin(X,x0);
assume
A1: X is infinite;
let U be Subset of DiscrWithInfin(X,x0);
assume
A2: U = {x0};
the carrier of T = X by Def5;
then X = U` \/ {x0} by A2,XBOOLE_1:45;
then
A3: U` is infinite by A1;
x0 in U by A2,TARSKI:def 1;
hence thesis by A3,Th19;
end;
theorem Th24:
for X,x0 being set for A being Subset of DiscrWithInfin(X,x0) st
A is finite holds Cl A = A
proof
let X,x0 be set;
let A be Subset of DiscrWithInfin(X,x0);
assume A is finite;
then A is closed by Th20;
hence thesis by PRE_TOPC:22;
end;
theorem Th25:
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}
proof
let T be non empty TopSpace;
let A be Subset of T such that
A1: A is not closed;
A2: A c= Cl A by PRE_TOPC:18;
let a be Point of T;
assume A \/ {a} is closed;
then
A3: Cl (A\/{a}) = A\/{a} by PRE_TOPC:22;
Cl A c= Cl (A\/{a}) by PRE_TOPC:19,XBOOLE_1:7;
hence thesis by A1,A2,A3,ZFMISC_1:138;
end;
theorem Th26:
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}
proof
let X,x0 be set such that
A1: x0 in X;
set T = DiscrWithInfin(X,x0);
reconsider T as non empty TopSpace by A1;
reconsider x = x0 as Point of T by A1,Def5;
let A be Subset of DiscrWithInfin(X,x0);
reconsider B = {x} as Subset of T;
reconsider A9 = A as Subset of T;
x0 in {x0} by TARSKI:def 1;
then x0 in A9 \/ B by XBOOLE_0:def 3;
then A9\/B is closed by Th20;
then
A2: Cl(A9\/B) = A9\/B by PRE_TOPC:22;
assume A is infinite;
then A9 is not closed or x0 in A by A1,Th20;
hence thesis by A2,Th25,ZFMISC_1:40;
end;
theorem
for X,x0 being set for A being Subset of DiscrWithInfin(X,x0) st A` is
finite holds Int A = A
proof
let X,x0 be set;
let A be Subset of DiscrWithInfin(X,x0);
assume A` is finite;
then Cl A` = A` by Th24;
hence Int A = A`` by TOPS_1:def 1
.= A;
end;
theorem
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}
proof
let X,x0 be set such that
A1: x0 in X;
set T = DiscrWithInfin(X,x0);
reconsider T as non empty TopSpace by A1;
reconsider x = x0 as Point of T by A1,Def5;
let A be Subset of DiscrWithInfin(X,x0);
reconsider A9 = A as Subset of T;
assume A` is infinite;
then Cl A` = A9` \/ {x} by A1,Th26;
hence Int A = (A9` \/ {x})` by TOPS_1:def 1
.= (A9 \ {x})`` by SUBSET_1:14
.= A \ {x0};
end;
theorem Th29:
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}
proof
let X, x0 be set;
set T = DiscrWithInfin(X,x0);
set B1 = (SmallestPartition X) \ {{x0}};
set B2 = {F` where F is Subset of X: F is finite};
A1: B1 c= the topology of T
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A2: a in B1;
then
A3: a in SmallestPartition X by ZFMISC_1:56;
then reconsider X as non empty set;
SmallestPartition X = the set of all {x} where x is Element of X
by EQREL_1:37;
then
A4: ex x being Element of X st a = {x} by A3;
a <> {x0} by A2,ZFMISC_1:56;
then not x0 in aa by A4,TARSKI:def 1;
then a is open Subset of T by A2,Def5,Th19;
hence thesis by PRE_TOPC:def 2;
end;
A5: the carrier of T = X by Def5;
B2 c= bool the carrier of T
proof
let a be object;
assume a in B2;
then ex F being Subset of X st a = F` & F is finite;
hence thesis by A5;
end;
then reconsider B0 = B1 \/ B2 as Subset-Family of T by A5,XBOOLE_1:8;
A6: now
let A be Subset of T;
assume A is open;
then
A7: not x0 in A or A` is finite by Th19;
let p be Point of T such that
A8: p in A;
reconsider X9 = X as non empty set by A8,Def5;
reconsider p9 = p as Element of X9 by Def5;
SmallestPartition X = the set of all {x} where x is Element of X9
by EQREL_1:37;
then
A9: {p9} in SmallestPartition X;
{p} <> {x0} or A`` in B2 by A5,A8,A7,ZFMISC_1:3;
then not {p} in {{x0}} or A in B2 by TARSKI:def 1;
then {p} in B1 or A in B2 by A9,XBOOLE_0:def 5;
then {p} in B0 & p in {p} & {p} c= A or A in B0 & A c= A by A8,
XBOOLE_0:def 3,ZFMISC_1:31;
hence ex a being Subset of T st a in B0 & p in a & a c= A by A8;
end;
B2 c= the topology of T
proof
let a be object;
assume a in B2;
then consider F being Subset of X such that
A10: a = F` and
A11: F is finite;
F`` is finite by A11;
then a is open Subset of T by A5,A10,Th19;
hence thesis by PRE_TOPC:def 2;
end;
then reconsider B0 as Basis of DiscrWithInfin(X,x0) by A1,A6,XBOOLE_1:8
,YELLOW_9:32;
take B0;
thus thesis;
end;
theorem
for X being infinite set holds card Fin X = card X
proof
deffunc f(set) = proj2 $1;
let X be infinite set;
set FX = Fin X;
consider f being Function such that
A1: dom f = X* & for a st a in X* holds f.a = f(a) from FUNCT_1:sch 5;
FX c= rng f
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A2: a in FX;
then aa is finite by FINSUB_1:def 5;
then consider p being FinSequence such that
A3: a = rng p by FINSEQ_1:52;
aa c= X by A2,FINSUB_1:def 5;
then p is FinSequence of X by A3,FINSEQ_1:def 4;
then
A4: p in X* by FINSEQ_1:def 11;
then f.p in rng f by A1,FUNCT_1:def 3;
hence thesis by A1,A3,A4;
end;
then card FX c= card (X*) by A1,CARD_1:12;
hence card FX c= card X by CARD_4:24;
set SX = SmallestPartition X;
SX c= FX
proof
let a be object;
assume a in SX;
then a in the set of all {x} where x is Element of X by EQREL_1:37;
then ex x being Element of X st a = {x};
hence thesis by FINSUB_1:def 5;
end;
then card SX c= card FX by CARD_1:11;
hence thesis by Th12;
end;
theorem Th31:
for X being infinite set holds card {F` where F is Subset of X:
F is finite} = card X
proof
let X be infinite set;
set FX = {F` where F is Subset of X: F is finite};
deffunc f(set) = X\proj2 $1;
consider f being Function such that
A1: dom f = X* & for a st a in X* holds f.a = f(a) from FUNCT_1:sch 5;
FX c= rng f
proof
let a be object;
assume a in FX;
then consider F being Subset of X such that
A2: a = F` and
A3: F is finite;
consider p being FinSequence such that
A4: F = rng p by A3,FINSEQ_1:52;
p is FinSequence of X by A4,FINSEQ_1:def 4;
then
A5: p in X* by FINSEQ_1:def 11;
then f.p in rng f by A1,FUNCT_1:def 3;
hence thesis by A1,A2,A4,A5;
end;
then card FX c= card (X*) by A1,CARD_1:12;
hence card FX c= card X by CARD_4:24;
deffunc f(set) = X\{$1};
consider f being Function such that
A6: dom f = X & for a st a in X holds f.a = f(a) from FUNCT_1:sch 5;
A7: rng f c= FX
proof
let a be object;
assume a in rng f;
then consider b being object such that
A8: b in dom f and
A9: a = f.b by FUNCT_1:def 3;
reconsider b as Element of X by A6,A8;
{b}` in FX;
hence thesis by A6,A9;
end;
f is one-to-one
proof
let a,b be object;
assume that
A10: a in dom f and
A11: b in dom f and
A12: f.a = f.b;
reconsider a,b as Element of X by A6,A10,A11;
{a}` = f.b by A6,A12
.= {b}` by A6;
then {a} = {b} by SUBSET_1:42;
hence thesis by ZFMISC_1:3;
end;
hence thesis by A6,A7,CARD_1:10;
end;
theorem Th32:
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
proof
let X be infinite set;
let x0 be set;
set T = DiscrWithInfin(X,x0);
let B0 be Basis of T;
set SX = SmallestPartition X, FX = {F` where F is Subset of X: F is finite};
assume
A1: B0 = (SX \ {{x0}}) \/ FX;
A2: card SX = card X by Th12;
A3: card {{x0}} = 1 by CARD_1:30;
A4: 1 in card X by CARD_3:86;
then card X +` 1 = card X by CARD_2:76;
then
A5: card (SX \ {{x0}}) = card X by A3,A2,A4,CARD_2:98;
card FX = card X by Th31;
then card B0 c= card X +` card X by A1,A5,CARD_2:34;
hence card B0 c= card X by CARD_2:75;
thus thesis by A1,A5,CARD_1:11,XBOOLE_1:7;
end;
theorem Th33:
for X being infinite set, x0 being set for B being Basis of
DiscrWithInfin(X,x0) holds card X c= card B
proof
let X be infinite set;
let x0 be set;
set T = DiscrWithInfin(X,x0);
set SX = SmallestPartition X;
A1: card {{x0}} = 1 by CARD_1:30;
A2: card SX = card X by Th12;
let B be Basis of T;
A3: the carrier of T = X by Def5;
A4: SX = the set of all {x} where x is Element of X by EQREL_1:37;
A5: SX\{{x0}} c= B
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A6: a in SX\{{x0}};
then not a in {{x0}} by XBOOLE_0:def 5;
then
A7: a <> {x0} by TARSKI:def 1;
a in SX by A6,XBOOLE_0:def 5;
then ex x being Element of X st a = {x} by A4;
then consider x being Element of T such that
A8: a = {x} and
A9: x <> x0 by A3,A7;
A10: x in aa by A8,TARSKI:def 1;
a is open Subset of T by A3,A8,A9,Th22;
then consider U being Subset of T such that
A11: U in B and
A12: x in U and
A13: U c= aa by A10,YELLOW_9:31;
aa c= U by A8,A12,ZFMISC_1:31;
hence thesis by A11,A13,XBOOLE_0:def 10;
end;
A14: 1 in card X by CARD_3:86;
then card X +` 1 = card X by CARD_2:76;
then card (SX \ {{x0}}) = card X by A1,A2,A14,CARD_2:98;
hence thesis by A5,CARD_1:11;
end;
theorem
for X being infinite set, x0 being set holds weight DiscrWithInfin(X,
x0) = card X
proof
let X be infinite set;
let x0 be set;
set T = DiscrWithInfin(X,x0);
consider B0 being Basis of T such that
A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ {F` where F is Subset of X:
F is finite} by Th29;
card B0 = card X by A1,Th32;
hence weight T c= card X by WAYBEL23:73;
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence thesis by Th33;
end;
theorem
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
proof
let X be non empty set;
let x0 be set;
set T = DiscrWithInfin(X,x0);
set SX = SmallestPartition X, FX = {F` where F is Subset of X: F is finite},
AX = the set of all {x}` where x is Element of X;
reconsider SX as Subset-Family of T by Def5;
AX c= bool X
proof
let a be object;
assume a in AX;
then ex x being Element of X st a = {x}`;
hence thesis;
end;
then reconsider AX as Subset-Family of T by Def5;
reconsider pB = (SX\{{x0}})\/AX as Subset-Family of T;
consider B0 being Basis of T such that
A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ FX by Th29;
A2: the carrier of T = X by Def5;
A3: FX c= FinMeetCl pB
proof
let a be object;
assume a in FX;
then consider F being Subset of T such that
A4: a = F` and
A5: F is finite by A2;
set SF = SmallestPartition F;
bool F c= bool X by A2,ZFMISC_1:67;
then reconsider SF as Subset-Family of T by A2,XBOOLE_1:1;
per cases;
suppose
F = {};
hence thesis by A4,CANTOR_1:8;
end;
suppose
F <> {};
then reconsider F as non empty Subset of T;
SF is a_partition of F;
then reconsider SF as non empty Subset-Family of T;
A6: COMPLEMENT SF c= pB
proof
let a be object;
assume
A7: a in COMPLEMENT SF;
then reconsider a as Subset of T;
a` in SF by A7,SETFAM_1:def 7;
then a` in the set of all {b} where b is Element of F by
EQREL_1:37;
then consider b being Element of F such that
A8: a` = {b};
reconsider b as Element of X by Def5;
{b}` in AX;
hence thesis by A2,A8,XBOOLE_0:def 3;
end;
F = union SF by EQREL_1:def 4;
then
A9: a = meet COMPLEMENT SF by A4,TOPS_2:6;
COMPLEMENT SF is finite by A5,TOPS_2:8;
then Intersect COMPLEMENT SF in FinMeetCl pB by A6,CANTOR_1:def 3;
hence thesis by A9,SETFAM_1:def 9;
end;
end;
A10: pB c= FinMeetCl pB by CANTOR_1:4;
A11: B0 c= FinMeetCl pB
proof
let a be object;
assume a in B0;
then a in SX\{{x0}} or a in FX by A1,XBOOLE_0:def 3;
then a in pB or a in FX by XBOOLE_0:def 3;
hence thesis by A10,A3;
end;
A12: B0 c= the topology of T by TOPS_2:64;
AX c= FX
proof
let a be object;
assume a in AX;
then ex x being Element of X st a = {x}`;
hence thesis;
end;
then pB c= B0 by A1,XBOOLE_1:9;
then pB c= the topology of T by A12;
then FinMeetCl pB c= FinMeetCl the topology of T by CANTOR_1:14;
then FinMeetCl pB c= the topology of T by CANTOR_1:5;
then FinMeetCl pB is Basis of T by A11,WAYBEL19:22;
then pB is prebasis of T by YELLOW_9:23;
hence thesis;
end;
begin :: Exercises
::<DSCR name="Exercise 1.1.B" monograph="topology"/>
theorem
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
}
proof
let T be TopSpace;
let F be Subset-Family of T;
let I be non empty Subset-Family of F;
set G0 = the Element of I;
reconsider G0 as Subset-Family of T by XBOOLE_1:1;
set Z = {Cl union G where G is Subset-Family of T: G in I};
A1: Cl union G0 in Z;
then reconsider Z9 = Z as non empty set;
assume
A2: for G being set st G in I holds F\G is finite;
thus Cl union F c= union clf F \/ meet Z
proof
let a be object;
assume that
A3: a in Cl union F and
A4: not a in union clf F \/ meet Z;
reconsider a as Point of T by A3;
not a in meet Z9 by A4,XBOOLE_0:def 3;
then consider b such that
A5: b in Z and
A6: not a in b by SETFAM_1:def 1;
consider G being Subset-Family of T such that
A7: b = Cl union G and
A8: G in I by A5;
A9: T is non empty by A3;
then clf (F\G) c= clf F by PCOMPS_1:14,XBOOLE_1:36;
then
A10: union clf (F\G) c= union clf F by ZFMISC_1:77;
F = G \/ (F\G) by A8,XBOOLE_1:45;
then union F = union G \/ union (F\G) by ZFMISC_1:78;
then Cl union F = Cl union G \/ Cl union (F\G) by PRE_TOPC:20;
then a in Cl union (F\G) by A3,A6,A7,XBOOLE_0:def 3;
then a in union clf (F\G) by A2,A8,A9,PCOMPS_1:16;
hence contradiction by A4,A10,XBOOLE_0:def 3;
end;
let a be object;
assume
A11: a in union clf F \/ meet Z;
per cases by A11,XBOOLE_0:def 3;
suppose
a in union clf F;
then consider b such that
A12: a in b and
A13: b in clf F by TARSKI:def 4;
ex W being Subset of T st b = Cl W & W in F by A13,PCOMPS_1:def 2;
then b c= Cl union F by PRE_TOPC:19,ZFMISC_1:74;
hence thesis by A12;
end;
suppose
A14: a in meet Z9;
union G0 c= union F by ZFMISC_1:77;
then
A15: Cl union G0 c= Cl union F by PRE_TOPC:19;
a in Cl union G0 by A1,A14,SETFAM_1:def 1;
hence thesis by A15;
end;
end;
::<DSCR name="Exercise 1.1.B" monograph="topology"/>
theorem
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}
proof
let T be TopSpace;
let F be Subset-Family of T;
set Z = {Cl union G where G is Subset-Family of T: G c= F & F\G is finite};
F\F = {} by XBOOLE_1:37;
then
A1: Cl union F in Z;
then reconsider Z9 = Z as non empty set;
thus Cl union F c= union clf F \/ meet Z
proof
let a be object;
assume that
A2: a in Cl union F and
A3: not a in union clf F \/ meet Z;
reconsider a as Point of T by A2;
not a in meet Z9 by A3,XBOOLE_0:def 3;
then consider b such that
A4: b in Z and
A5: not a in b by SETFAM_1:def 1;
consider G being Subset-Family of T such that
A6: b = Cl union G and
A7: G c= F and
A8: F\G is finite by A4;
A9: T is non empty by A2;
then clf (F\G) c= clf F by PCOMPS_1:14,XBOOLE_1:36;
then
A10: union clf (F\G) c= union clf F by ZFMISC_1:77;
F = G \/ (F\G) by A7,XBOOLE_1:45;
then union F = union G \/ union (F\G) by ZFMISC_1:78;
then Cl union F = Cl union G \/ Cl union (F\G) by PRE_TOPC:20;
then a in Cl union (F\G) by A2,A5,A6,XBOOLE_0:def 3;
then a in union clf (F\G) by A8,A9,PCOMPS_1:16;
hence contradiction by A3,A10,XBOOLE_0:def 3;
end;
let a be object;
assume
A11: a in union clf F \/ meet Z;
per cases by A11,XBOOLE_0:def 3;
suppose
a in union clf F;
then consider b such that
A12: a in b and
A13: b in clf F by TARSKI:def 4;
ex W being Subset of T st b = Cl W & W in F by A13,PCOMPS_1:def 2;
then b c= Cl union F by PRE_TOPC:19,ZFMISC_1:74;
hence thesis by A12;
end;
suppose
a in meet Z9;
hence thesis by A1,SETFAM_1:def 1;
end;
end;
::<DSCR name="Exercise 1.1.D" monograph="topology"/>
theorem
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
proof
let X be set;
let O be Subset-Family of bool X such that
A1: for o being Subset-Family of X st o in O holds TopStruct(#X,o#) is
TopSpace;
reconsider B = Intersect O as Subset-Family of X;
set T = TopStruct(#X,B#);
take B;
thus B = Intersect O;
A2: T is TopSpace-like
proof
now
thus the carrier of T in bool the carrier of T by ZFMISC_1:def 1;
let a;
assume
A3: a in O;
then reconsider o = a as Subset-Family of X;
TopStruct(#X,o#) is TopSpace by A1,A3;
hence the carrier of T in a by PRE_TOPC:def 1;
end;
hence the carrier of T in the topology of T by SETFAM_1:43;
hereby
let a be Subset-Family of T such that
A4: a c= the topology of T;
now
let b;
assume
A5: b in O;
then reconsider o = b as Subset-Family of X;
B c= b by A5,MSSUBFAM:2;
then
A6: a c= o by A4;
TopStruct(#X,o#) is TopSpace by A1,A5;
hence union a in b by A6,PRE_TOPC:def 1;
end;
hence union a in the topology of T by SETFAM_1:43;
end;
let a,b be Subset of T such that
A7: a in the topology of T and
A8: b in the topology of T;
now
let c;
assume
A9: c in O;
then reconsider o = c as Subset-Family of X;
A10: b in o by A8,A9,SETFAM_1:43;
A11: TopStruct(#X,o#) is TopSpace by A1,A9;
a in o by A7,A9,SETFAM_1:43;
hence a /\ b in c by A10,A11,PRE_TOPC:def 1;
end;
hence thesis by SETFAM_1:43;
end;
hence T is TopSpace;
thus for o being Subset-Family of X st o in O holds TopStruct(#X,o#) is
TopExtension of T
proof
let o be Subset-Family of X such that
A12: o in O;
reconsider S = TopStruct(#X,o#) as TopSpace by A1,A12;
Intersect O c= o by A12,MSSUBFAM:2;
then S is TopExtension of T by YELLOW_9:def 5;
hence thesis;
end;
reconsider TT = T as TopSpace by A2;
let T9 be TopSpace such that
A13: the carrier of T9 = X and
A14: for o being Subset-Family of X st o in O holds TopStruct(#X,o#) is
TopExtension of T9;
now
let a;
assume
A15: a in O;
then reconsider o = a as Subset-Family of X;
TopStruct(#X,o#) is TopExtension of T9 by A14,A15;
hence the topology of T9 c= a by YELLOW_9:def 5;
end;
then the topology of T9 c= Intersect O by A13,MSSUBFAM:4;
then TT is TopExtension of T9 by A13,YELLOW_9:def 5;
hence thesis;
end;
::<DSCR name="Exercise 1.1.D" monograph="topology"/>
theorem
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#)
proof
reconsider e = {} bool {}, tE = {{}{}} as Subset-Family of {};
reconsider E = {} bool bool {} as empty Subset-Family of bool {};
let X be set;
let O be Subset-Family of bool X;
reconsider B = UniCl FinMeetCl union O as Subset-Family of X;
take B;
thus B = UniCl FinMeetCl union O;
reconsider dT = TopStruct(#{},tE#) as discrete TopStruct by TDLAT_3:def 1
,ZFMISC_1:1;
A1: {{},{}} = tE by ENUMSET1:29;
A2: FinMeetCl tE = {{},{}} by YELLOW_9:11;
A3: now
assume
A4: X is empty;
hence
A5: union O = e or union O = tE by ZFMISC_1:1,33;
thus FinMeetCl union E = the topology of dT by YELLOW_9:17;
hence TopStruct(#X,B#) is TopSpace by A2,A1,A4,A5,YELLOW_9:11;
end;
hence TopStruct(#X,B#) is TopSpace by CANTOR_1:15;
reconsider TT = TopStruct(#X,B#) as TopSpace by A3,CANTOR_1:15;
hereby
let o be Subset-Family of X;
set S = TopStruct(#X,o#);
A6: FinMeetCl union O c= B by CANTOR_1:1;
assume o in O;
then
A7: o c= union O by ZFMISC_1:74;
union O c= FinMeetCl union O by CANTOR_1:4;
then o c= FinMeetCl union O by A7;
then the topology of S c= the topology of TT by A6;
hence TopStruct(#X,B#) is TopExtension of S by YELLOW_9:def 5;
end;
let T be TopSpace such that
A8: the carrier of T = X and
A9: for o being Subset-Family of X st o in O holds T is TopExtension of
TopStruct(#X,o#);
thus the carrier of T = the carrier of TopStruct(#X,B#) by A8;
A10: X <> {} implies T is non empty by A8;
now
let a;
assume
A11: a in O;
then reconsider o = a as Subset-Family of X;
T is TopExtension of TopStruct(#X,o#) by A9,A11;
hence a c= the topology of T by YELLOW_9:def 5;
end;
then union O c= the topology of T by ZFMISC_1:76;
then FinMeetCl union O c= FinMeetCl the topology of T by A8,CANTOR_1:14;
then
A12: B c= UniCl FinMeetCl the topology of T by A8,CANTOR_1:9;
X in the topology of T by A8,PRE_TOPC:def 1;
hence thesis by A12,A10,CANTOR_1:7;
end;