:: Paracompact and Metrizable Spaces
:: by Leszek Borys
::
:: Received June 8, 1991
:: Copyright (c) 1991-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 NUMBERS, METRIC_1, SUBSET_1, REAL_1, XXREAL_0, TARSKI, ARYTM_3,
XBOOLE_0, PRE_TOPC, SETFAM_1, ZFMISC_1, COMPTS_1, STRUCT_0, RCOMP_1,
FINSET_1, FINSEQ_1, RELAT_1, NAT_1, CARD_1, FUNCT_1, CARD_5, ARYTM_1,
PCOMPS_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, REAL_1, TOPS_2, SETFAM_1, DOMAIN_1, STRUCT_0,
FINSET_1, COMPTS_1, PRE_TOPC, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1,
FINSEQ_1, NAT_1, METRIC_1;
constructors SETFAM_1, DOMAIN_1, REAL_1, SQUARE_1, NAT_1, MEMBERED, FINSEQ_1,
TOPS_2, COMPTS_1, METRIC_1, RELSET_1, BINOP_1, BINOP_2, VALUED_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0,
NAT_1, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, FINSEQ_1, PRE_TOPC, RELAT_1,
ORDINAL1, BINOP_2, VALUED_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities STRUCT_0, COMPTS_1, SUBSET_1, RELAT_1;
expansions TARSKI, COMPTS_1;
theorems PRE_TOPC, TOPS_1, TOPS_2, NAT_1, FINSET_1, SUBSET_1, SETFAM_1,
TARSKI, FINSEQ_1, ZFMISC_1, FUNCT_1, FUNCT_2, METRIC_1, RELAT_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0;
schemes SUBSET_1, FUNCT_2, NAT_1;
begin
reserve PM for MetrStruct;
reserve x,y for Element of PM;
reserve r,p,q,s,t for Real;
theorem Th1:
for r, p being Real st r <= p holds Ball(x,r) c= Ball(x,p)
proof
let r, p be Real;
assume
A1: r <= p;
for y holds y in Ball(x,r) implies y in Ball(x,p)
proof
let y;
assume
A2: y in Ball(x,r);
then dist(x,y) < r by METRIC_1:11;
then
A3: dist(x,y) < p by A1,XXREAL_0:2;
PM is non empty by A2;
hence thesis by A3,METRIC_1:11;
end;
hence thesis;
end;
reserve T for TopSpace;
reserve A for Subset of T;
theorem Th2:
Cl(A) <> {} iff A <> {}
proof
A <> {} implies Cl(A) <> {}
proof
set x = the Element of A;
A1: A c= Cl A by PRE_TOPC:18;
assume
A2: A <> {};
ex x be set st x in Cl A
proof
take x;
thus thesis by A2,A1;
end;
hence thesis;
end;
hence thesis by PRE_TOPC:22;
end;
reserve T for non empty TopSpace;
reserve x for Point of T;
reserve Z,X,V,W,Y,Q for Subset of T;
reserve FX for Subset-Family of T;
theorem Th3:
FX is Cover of T implies for x ex W st x in W & W in FX
proof
assume FX is Cover of T;
then
A1: union FX = [#](T) by SETFAM_1:45;
thus thesis
proof
let x;
thus ex W st x in W & W in FX
proof
consider W being set such that
A2: x in W and
A3: W in FX by A1,TARSKI:def 4;
reconsider W as Subset of T by A3;
take W;
thus thesis by A2,A3;
end;
end;
end;
reserve a for set;
theorem
the topology of 1TopSp a = bool a;
theorem
the carrier of 1TopSp a = a;
theorem
1TopSp {a} is compact;
theorem
T is T_2 implies {x} is closed;
:: Paracompact spaces
reserve x,y for Point of T;
reserve A,B for Subset of T;
reserve FX,GX for Subset-Family of T;
definition
let T be TopStruct;
let IT be Subset-Family of T;
attr IT is locally_finite means
for x being Point of T ex W being
Subset of T st x in W & W is open & { V where V is Subset of T: V in IT & V
meets W } is finite;
end;
theorem Th8:
for W holds { V : V in FX & V meets W} c= FX
proof
let W;
now
let Y be object;
assume Y in { V : V in FX & V meets W };
then ex V st Y = V & V in FX & V meets W;
hence Y in FX;
end;
hence thesis;
end;
theorem Th9:
FX c= GX & GX is locally_finite implies FX is locally_finite
proof
assume that
A1: FX c= GX and
A2: GX is locally_finite;
now
let x;
thus ex W being Subset of T st x in W & W is open & { V : V in FX & V
meets W } is finite
proof
consider Y being Subset of T such that
A3: x in Y and
A4: Y is open and
A5: { X : X in GX & X meets Y } is finite by A2;
take W = Y;
thus x in W by A3;
thus W is open by A4;
{ V : V in FX & V meets W } c= { X : X in GX & X meets Y }
proof
let Z be object;
assume
A6: Z in { V : V in FX & V meets W };
ex X st Z = X & X in GX & X meets Y
proof
consider V such that
A7: Z = V and
A8: V in FX and
A9: V meets W by A6;
take X = V;
thus Z = X by A7;
thus X in GX by A1,A8;
thus thesis by A9;
end;
hence Z in { X : X in GX & X meets Y };
end;
hence thesis by A5;
end;
end;
hence thesis;
end;
theorem Th10:
FX is finite implies FX is locally_finite
proof
assume
A1: FX is finite;
for x ex W being Subset of T st x in W & W is open & { V : V in FX & V
meets W } is finite
proof
let x;
take [#]T;
thus x in [#]T;
thus [#]T is open;
thus thesis by A1,Th8,FINSET_1:1;
end;
hence thesis;
end;
definition
let T be TopStruct, FX be Subset-Family of T;
func clf FX -> Subset-Family of T means
:Def2:
for Z being Subset of T holds
Z in it iff ex W being Subset of T st Z = Cl W & W in FX;
existence
proof
defpred P[set] means ex W being Subset of T st $1 = Cl W & W in FX;
thus ex S be Subset-Family of T st for Z be Subset of T holds Z in S iff P
[Z] from SUBSET_1:sch 3;
end;
uniqueness
proof
let HX,GX be Subset-Family of T;
assume that
A1: for Z being Subset of T holds Z in HX iff ex W being Subset of T
st Z = Cl W & W in FX and
A2: for X being Subset of T holds X in GX iff ex V being Subset of T
st X = Cl V & V in FX;
now
let X be object;
assume
A3: X in GX;
then reconsider X9=X as Subset of T;
ex V being Subset of T st X9 = Cl V & V in FX by A2,A3;
hence X in HX by A1;
end;
then
A4: GX c= HX;
now
let Z be object;
assume
A5: Z in HX;
then reconsider Z9=Z as Subset of T;
ex W being Subset of T st Z9 = Cl W & W in FX by A1,A5;
hence Z in GX by A2;
end;
then HX c= GX;
hence thesis by A4,XBOOLE_0:def 10;
end;
end;
theorem
for T being TopSpace, FX being Subset-Family of T holds clf FX is closed
proof
let T be TopSpace, FX be Subset-Family of T;
for V being Subset of T st V in clf FX holds V is closed
proof
let V be Subset of T;
assume V in clf FX;
then ex W being Subset of T st V = Cl W & W in FX by Def2;
hence thesis;
end;
hence thesis by TOPS_2:def 2;
end;
theorem Th12:
for T being TopSpace, FX being Subset-Family of T st FX = {}
holds clf FX = {}
proof
let T be TopSpace, FX be Subset-Family of T;
reconsider CFX = clf FX as set;
set X = the Element of CFX;
assume
A1: FX = {};
A2: for X be set holds not X in CFX
proof
let X be set;
assume
A3: X in CFX;
then reconsider X as Subset of T;
ex V being Subset of T st X = Cl V & V in FX by A3,Def2;
hence thesis by A1;
end;
assume not thesis;
then X in CFX;
hence contradiction by A2;
end;
theorem Th13:
FX = { V } implies clf FX = { Cl V }
proof
reconsider CFX = clf FX as set;
assume
A1: FX = { V };
for W be object holds W in CFX iff W = Cl V
proof
let W be object;
A2: W = Cl V implies W in CFX
proof
assume
A3: W = Cl V;
ex X st W = Cl X & X in FX
proof
take V;
thus thesis by A1,A3,TARSKI:def 1;
end;
hence thesis by Def2;
end;
W in CFX implies W = Cl V
proof
assume
A4: W in CFX;
then reconsider W as Subset of T;
ex X st W = Cl X & X in FX by A4,Def2;
hence thesis by A1,TARSKI:def 1;
end;
hence thesis by A2;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th14:
FX c= GX implies clf FX c= clf GX
proof
reconsider CFX = clf FX,CGX = clf GX as set;
assume
A1: FX c= GX;
for X be object st X in CFX holds X in CGX
proof
let X be object;
assume
A2: X in CFX;
then reconsider X as Subset of T;
ex V st X = Cl V & V in FX by A2,Def2;
hence thesis by A1,Def2;
end;
hence thesis;
end;
theorem Th15:
clf(FX \/ GX) = (clf FX) \/ (clf GX)
proof
for X be object holds X in clf(FX \/ GX) iff X in (clf FX) \/ (clf GX)
proof
let X be object;
A1: now
assume
A2: X in (clf FX) \/ (clf GX);
now
per cases by A2,XBOOLE_0:def 3;
suppose
A3: X in clf FX;
then reconsider X9= X as Subset of T;
ex W st X9 = Cl W & W in (FX \/ GX)
proof
consider Z such that
A4: X9 = Cl Z & Z in FX by A3,Def2;
take Z;
thus thesis by A4,XBOOLE_0:def 3;
end;
hence X in clf(FX \/ GX) by Def2;
end;
suppose
A5: X in clf GX;
then reconsider X9= X as Subset of T;
ex W st X9 = Cl W & W in (FX \/ GX)
proof
consider Z such that
A6: X9 = Cl Z & Z in GX by A5,Def2;
take Z;
thus thesis by A6,XBOOLE_0:def 3;
end;
hence X in clf(FX \/ GX) by Def2;
end;
end;
hence X in clf(FX \/ GX);
end;
now
assume
A7: X in clf(FX \/ GX);
then reconsider X9= X as Subset of T;
consider W such that
A8: X9 = Cl W and
A9: W in (FX \/ GX) by A7,Def2;
now
per cases by A9,XBOOLE_0:def 3;
suppose
W in FX;
then X9 in clf FX by A8,Def2;
hence X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def 3;
end;
suppose
W in GX;
then X9 in clf GX by A8,Def2;
hence X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def 3;
end;
end;
hence X in (clf FX) \/ (clf GX);
end;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th16:
FX is finite implies Cl(union FX) = union (clf FX)
proof
assume FX is finite;
then consider p being FinSequence such that
A1: rng p = FX by FINSEQ_1:52;
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def 2;
defpred P[Nat] means for GX st GX = p.:(Seg $1) & $1 <= n & 1 <= n holds Cl(
union GX) = union (clf GX);
A3: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume
A4: for GX st GX = p.:(Seg k) & k <= n & 1 <= n holds Cl(union GX) =
union (clf GX);
let GX such that
A5: GX = p.:(Seg(k+1));
assume that
A6: k+1 <= n and
A7: 1 <= n;
now
reconsider G2 = Im(p,k+1) as Subset-Family of T by A1,RELAT_1:111
,TOPS_2:2;
reconsider G1 = p.:(Seg k) as Subset-Family of T by A1,RELAT_1:111
,TOPS_2:2;
k+1 <= n+1 by A6,NAT_1:12;
then
A8: k <= n by XREAL_1:6;
0+1 = 1;
then 1 <= k+1 by XREAL_1:7;
then k+1 in dom p by A2,A6,FINSEQ_1:1;
then
A9: G2 = {p.(k+1)} by FUNCT_1:59;
then union G2 = p.(k+1) by ZFMISC_1:25;
then reconsider G3 = p.(k+1) as Subset of T;
A10: union (clf G2) = union { Cl G3 } by A9,Th13
.= Cl G3 by ZFMISC_1:25
.= Cl (union G2) by A9,ZFMISC_1:25;
A11: p.:(Seg(k+1)) = p.:(Seg k \/ {k+1}) by FINSEQ_1:9
.= p.:(Seg k) \/ p.:{k+1} by RELAT_1:120;
then Cl( union GX) = Cl( union G1 \/ union G2) by A5,ZFMISC_1:78
.= Cl( union G1 ) \/ Cl( union G2 ) by PRE_TOPC:20;
then Cl( union GX ) = union (clf G1) \/ union (clf G2) by A4,A7,A10,A8;
then Cl( union GX ) = union ((clf G1) \/ (clf G2)) by ZFMISC_1:78;
hence thesis by A5,A11,Th15;
end;
hence thesis;
end;
A12: P[0]
proof
let GX;
assume that
A13: GX = p.:(Seg 0) and
0 <= n and
1 <= n;
union GX = {}(T) by A13,ZFMISC_1:2;
then Cl(union GX) = {}(T) by PRE_TOPC:22;
hence thesis by A13,Th12,ZFMISC_1:2;
end;
A14: for k being Nat holds P[k] from NAT_1:sch 2(A12,A3);
A15: now
assume
A16: 1 <= n;
FX = p.:(Seg n) by A1,A2,RELAT_1:113;
hence thesis by A14,A16;
end;
A17: now
assume n = 0;
then Seg n = {};
then
A18: FX = p.:{} by A1,A2,RELAT_1:113;
then union FX = {}(T) by ZFMISC_1:2;
then Cl(union FX) = {}(T) by PRE_TOPC:22;
hence thesis by A18,Th12,ZFMISC_1:2;
end;
now
A19: 1 = 0+1;
assume n <> 0;
hence 1 <= n by A19,NAT_1:13;
end;
hence thesis by A15,A17;
end;
theorem Th17:
FX is_finer_than clf FX
proof
set GX = clf FX;
for X be set st X in FX ex Y be set st Y in GX & X c= Y
proof
let X be set;
assume
A1: X in FX;
then reconsider X as Subset of T;
thus thesis
proof
reconsider Y = Cl X as set;
take Y;
thus Y in GX by A1,Def2;
thus thesis by PRE_TOPC:18;
end;
end;
hence thesis by SETFAM_1:def 2;
end;
scheme
Lambda1top{T()->TopSpace, X()->Subset-Family of T(), Y()->Subset-Family of T
(), F(object)->Subset of T()}:
ex f being Function of X(),Y() st for Z being
Subset of T() st Z in X() holds f.Z = F(Z)
provided
A1: for Z being Subset of T() st Z in X() holds F(Z) in Y();
A2: for x be object st x in X() holds F(x) in Y() by A1;
consider f being Function of X(),Y() such that
A3: for x be object st x in X() holds f.x = F(x) from FUNCT_2:sch 2(A2);
take f;
thus thesis by A3;
end;
theorem
FX is locally_finite implies clf FX is locally_finite
proof
set GX = (clf FX);
assume
A1: FX is locally_finite;
for x ex W being Subset of T st x in W & W is open & { V : V in GX & V
meets W } is finite
proof
let x;
thus thesis
proof
deffunc G(Subset of T) = Cl $1;
consider W being Subset of T such that
A2: x in W and
A3: W is open and
A4: { V : V in FX & V meets W } is finite by A1;
take W;
thus x in W by A2;
thus W is open by A3;
set CGX = { V : V in GX & V meets W }, CFX = { V : V in FX & V meets W };
A5: for Y st Y in FX holds G(Y) in GX by Def2;
consider f be Function of FX,GX such that
A6: for X st X in FX holds f.X = G(X) from Lambda1top(A5);
A7: GX = {} implies FX = {} by Th17,SETFAM_1:16;
then
A8: dom f = FX by FUNCT_2:def 1;
for Z be object holds Z in f.:CFX iff Z in CGX
proof
let Z be object;
A9: Z in CGX implies Z in f.:CFX
proof
assume
A10: Z in CGX;
ex Y be set st Y in dom f & Y in CFX & Z = f.Y
proof
consider V such that
A11: Z = V and
A12: V in GX and
A13: V meets W by A10;
consider X such that
A14: V = Cl X and
A15: X in FX by A12,Def2;
take X;
A16: V /\ W <> {} by A13,XBOOLE_0:def 7;
ex Q st X = Q & Q in FX & Q meets W
proof
take Q = X;
thus X = Q;
thus Q in FX by A15;
Cl(W /\ (Cl Q)) <> {} by A16,A14,Th2;
then Cl(W /\ Q) <> {} by A3,TOPS_1:14;
then Q /\ W <> {} by Th2;
hence thesis by XBOOLE_0:def 7;
end;
hence thesis by A6,A7,A11,A14,FUNCT_2:def 1;
end;
hence thesis by FUNCT_1:def 6;
end;
Z in f.:CFX implies Z in CGX
proof
assume Z in f.:CFX;
then consider Y be object such that
A17: Y in dom f and
A18: Y in CFX and
A19: Z = f.Y by FUNCT_1:def 6;
reconsider Y as Subset of T by A8,A17;
A20: f.Y = Cl Y by A6,A8,A17;
then reconsider Z as Subset of T by A19;
ex V st Y = V & V in FX & V meets W by A18;
then
A21: Z meets W by A19,A20,PRE_TOPC:18,XBOOLE_1:63;
Z in GX by A8,A17,A19,A20,Def2;
hence thesis by A21;
end;
hence thesis by A9;
end;
hence thesis by A4,TARSKI:2;
end;
end;
hence thesis;
end;
theorem
union FX c= union(clf FX) by Th17,SETFAM_1:13;
theorem Th20:
FX is locally_finite implies Cl union FX = union clf FX
proof
set UFX = Cl(union FX), UCFX = union(clf FX);
assume
A1: FX is locally_finite;
for x st x in UFX holds x in UCFX
proof
let x;
consider W being Subset of T such that
A2: x in W & W is open and
A3: { V : V in FX & V meets W } is finite by A1;
set HX = { V : V in FX & V meets W };
reconsider HX as Subset-Family of T by Th8,TOPS_2:2;
A4: Cl(union HX) = union(clf HX) by A3,Th16;
set FHX = FX\HX;
A5: not x in Cl(union (FHX))
proof
assume
A6: x in Cl union (FHX);
reconsider FHX as set;
for Z be set st Z in FHX holds Z misses W
proof
let Z be set;
assume
A7: Z in FHX;
then reconsider Z as Subset of T;
Z in FX & not Z in HX by A7,XBOOLE_0:def 5;
hence thesis;
end;
then (union FHX) misses W by ZFMISC_1:80;
hence thesis by A2,A6,TOPS_1:12;
end;
HX \/ (FX \ HX) = HX \/ FX by XBOOLE_1:39
.= FX by Th8,XBOOLE_1:12;
then
A8: Cl(union FX) = Cl(union HX \/ union (FX \ HX)) by ZFMISC_1:78
.= (Cl union HX) \/ Cl(union (FX \ HX)) by PRE_TOPC:20;
clf HX c= clf FX by Th8,Th14;
then
A9: union(clf HX) c= union(clf FX) by ZFMISC_1:77;
assume x in UFX;
then x in Cl(union HX) by A5,A8,XBOOLE_0:def 3;
hence thesis by A4,A9;
end;
then
A10: UFX c= UCFX;
for x st x in UCFX holds x in UFX
proof
let x;
assume x in UCFX;
then consider X be set such that
A11: x in X and
A12: X in clf FX by TARSKI:def 4;
reconsider X as Subset of T by A12;
consider Y such that
A13: X = Cl Y and
A14: Y in FX by A12,Def2;
for A being Subset of T st A is open & x in A holds (union FX) meets A
proof
let A be Subset of T;
assume
A15: A is open & x in A;
ex y st y in (union FX) /\ A
proof
Y meets A by A11,A13,A15,TOPS_1:12;
then consider z be object such that
A16: z in Y /\ A by XBOOLE_0:4;
z in Y by A16,XBOOLE_0:def 4;
then
A17: z in union FX by A14,TARSKI:def 4;
take z;
z in A by A16,XBOOLE_0:def 4;
hence thesis by A17,XBOOLE_0:def 4;
end;
hence thesis by XBOOLE_0:4;
end;
hence thesis by TOPS_1:12;
end;
then UCFX c= UFX;
hence thesis by A10,XBOOLE_0:def 10;
end;
theorem
FX is locally_finite & FX is closed implies union FX is closed
proof
assume that
A1: FX is locally_finite and
A2: FX is closed;
union (clf FX) c= union FX
proof
set UFX = union FX, UCFX = union(clf FX);
for x st x in UCFX holds x in UFX
proof
let x;
assume x in UCFX;
then consider X be set such that
A3: x in X and
A4: X in clf FX by TARSKI:def 4;
reconsider X as Subset of T by A4;
consider W being Subset of T such that
A5: X = Cl W and
A6: W in FX by A4,Def2;
reconsider W as Subset of T;
W is closed by A2,A6,TOPS_2:def 2;
then x in W by A3,A5,PRE_TOPC:22;
hence thesis by A6,TARSKI:def 4;
end;
hence thesis;
end;
then
A7: Cl(union FX) c= union FX by A1,Th20;
union FX c= union(clf FX) by Th17,SETFAM_1:13;
then union FX c= Cl(union FX) by A1,Th20;
hence thesis by A7,XBOOLE_0:def 10;
end;
definition
let IT be TopStruct;
attr IT is paracompact means
for FX being Subset-Family of IT st FX
is Cover of IT & FX is open ex GX being Subset-Family of IT st GX is open & GX
is Cover of IT & GX is_finer_than FX & GX is locally_finite;
end;
registration
cluster paracompact for non empty TopSpace;
existence
proof
take PT = 1TopSp {1};
let FX be Subset-Family of PT;
assume that
A1: FX is Cover of PT and
FX is open;
consider GX being Subset-Family of PT such that
A2: GX c= FX & GX is Cover of PT and
GX is finite by A1;
take GX;
thus thesis by A2,Th10,SETFAM_1:12,TOPS_2:11;
end;
end;
theorem
T is compact implies T is paracompact
proof
assume
A1: T is compact;
for FX st FX is Cover of T & FX is open ex GX st GX is open & GX is
Cover of T & GX is_finer_than FX & GX is locally_finite
proof
let FX;
assume that
A2: FX is Cover of T and
A3: FX is open;
consider GX such that
A4: GX c= FX and
A5: GX is Cover of T and
A6: GX is finite by A1,A2,A3;
take GX;
for W being Subset of T st W in GX holds W is open by A3,A4,TOPS_2:def 1;
hence GX is open by TOPS_2:def 1;
thus GX is Cover of T by A5;
thus GX is_finer_than FX by A4,SETFAM_1:12;
thus thesis by A6,Th10;
end;
hence thesis;
end;
theorem Th23:
T is paracompact & B is closed & (for x st x in B ex V,W being
Subset of T st V is open & W is open & A c= V & x in W & V misses W) implies ex
Y,Z being Subset of T st Y is open & Z is open & A c=Y & B c= Z & Y misses Z
proof
assume that
A1: T is paracompact and
A2: B is closed and
A3: for x st x in B ex V,W being Subset of T st V is open & W is open &
A c= V & x in W & V misses W;
defpred P[set] means $1=B` or ex V,W being Subset of T, x st x in B & $1 = W
& V is open & W is open & A c= V & x in W & V misses W;
consider GX such that
A4: for X being Subset of T holds X in GX iff P[X] from SUBSET_1:sch 3;
now
let x;
assume x in [#](T);
then
A5: x in B \/ B` by PRE_TOPC:2;
now
per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in B;
ex X st x in X & X in GX
proof
consider V,W being Subset of T such that
A7: V is open & W is open & A c= V and
A8: x in W and
A9: V misses W by A3,A6;
take X = W;
thus x in X by A8;
thus thesis by A4,A6,A7,A8,A9;
end;
hence x in union GX by TARSKI:def 4;
end;
suppose
A10: x in B`;
ex X st x in X & X in GX
proof
take X=B`;
thus x in X by A10;
thus thesis by A4;
end;
hence x in union GX by TARSKI:def 4;
end;
end;
hence x in union GX;
end;
then [#](T) c= union GX;
then [#](T) = union GX by XBOOLE_0:def 10;
then
A11: GX is Cover of T by SETFAM_1:45;
for X being Subset of T st X in GX holds X is open
proof
let X be Subset of T;
assume
A12: X in GX;
now
per cases by A4,A12;
suppose
X = B`;
hence thesis by A2;
end;
suppose
ex V,W being Subset of T, y st y in B & X = W & V is open & W
is open & A c= V & y in W & V misses W;
hence thesis;
end;
end;
hence thesis;
end;
then GX is open by TOPS_2:def 1;
then consider FX such that
A13: FX is open and
A14: FX is Cover of T and
A15: FX is_finer_than GX and
A16: FX is locally_finite by A1,A11;
set HX = { W : W in FX & W meets B};
A17: HX c= FX by Th8;
reconsider HX as Subset-Family of T by Th8,TOPS_2:2;
take Y = (union (clf HX))`;
take Z = union HX;
union (clf HX) = Cl (union HX) by A16,A17,Th9,Th20;
hence Y is open;
thus Z is open by A13,A17,TOPS_2:11,19;
A18: for X st X in HX holds A /\ Cl X = {}
proof
let X;
assume X in HX;
then
A19: ex W st W = X & W in FX & W meets B;
then consider Y being set such that
A20: Y in GX and
A21: X c= Y by A15,SETFAM_1:def 2;
reconsider Y as Subset of T by A20;
now
per cases by A4,A20;
suppose
Y = B`;
hence thesis by A19,A21,XBOOLE_1:63,79;
end;
suppose
ex V,W being Subset of T, y st y in B & Y = W & V is open & W
is open & A c= V & y in W & V misses W;
then consider V,W being Subset of T, y such that
y in B and
A22: Y = W and
A23: V is open and
W is open and
A24: A c= V and
y in W and
A25: V misses W;
V misses X by A21,A22,A25,XBOOLE_1:63;
then Cl(V /\ X) = Cl({}(T)) by XBOOLE_0:def 7;
then Cl(V /\ X) = {} by PRE_TOPC:22;
then Cl(V /\ Cl X) = {} by A23,TOPS_1:14;
then V /\ (Cl X) = {} by Th2;
then (Cl X) misses V by XBOOLE_0:def 7;
then A misses (Cl X) by A24,XBOOLE_1:63;
hence thesis by XBOOLE_0:def 7;
end;
end;
hence thesis;
end;
A misses (union (clf HX))
proof
assume A meets (union (clf HX));
then consider x being object such that
A26: x in A and
A27: x in union clf HX by XBOOLE_0:3;
reconsider x as Point of T by A26;
now
assume x in (union (clf HX));
then consider X being set such that
A28: x in X and
A29: X in (clf HX) by TARSKI:def 4;
reconsider X as Subset of T by A29;
ex W st X = Cl W & W in HX by A29,Def2;
then A /\ X = {} by A18;
then A misses X by XBOOLE_0:def 7;
hence not x in A by A28,XBOOLE_0:3;
end;
hence thesis by A26,A27;
end;
hence A c= Y by SUBSET_1:23;
now
let y;
assume
A30: y in B;
ex W st y in W & W in HX
proof
consider W such that
A31: y in W and
A32: W in FX by A14,Th3;
take W;
thus y in W by A31;
W meets B by A30,A31,XBOOLE_0:3;
hence thesis by A32;
end;
hence y in Z by TARSKI:def 4;
end;
hence B c= Z;
Z c= Y` by Th17,SETFAM_1:13;
hence Y misses Z by SUBSET_1:23;
end;
theorem Th24:
T is T_2 & T is paracompact implies T is regular
proof
assume
A1: T is T_2;
assume
A2: T is paracompact;
for x for A being Subset of T st A <> {} & A is closed & x in A` ex W,V
being Subset of T st W is open & V is open & x in W & A c= V & W misses V
proof
let x;
let A be Subset of T;
assume that
A <> {} and
A3: A is closed and
A4: x in A`;
set B = { x };
A5: not x in A by A4,XBOOLE_0:def 5;
for y st y in A ex V,W being Subset of T st V is open & W is open & B
c= V & y in W & V misses W
proof
let y;
assume y in A;
then consider V,W being Subset of T such that
A6: V is open & W is open & x in V & y in W & V misses W by A1,A5,
PRE_TOPC:def 10;
take V,W;
thus thesis by A6,ZFMISC_1:31;
end;
then consider Y,Z being Subset of T such that
A7: Y is open & Z is open & B c= Y & A c= Z & Y misses Z by A2,A3,Th23;
take Y,Z;
thus thesis by A7,ZFMISC_1:31;
end;
hence thesis;
end;
theorem
T is T_2 & T is paracompact implies T is normal
proof
assume that
A1: T is T_2 and
A2: T is paracompact;
for A,B being Subset of T st A <> {} & B <> {} & A is closed & B is
closed & A misses B ex W,V being Subset of T st W is open & V is open & A c= W
& B c= V & W misses V
proof
let A,B be Subset of T;
assume that
A3: A <> {} and
B <> {} and
A4: A is closed and
A5: B is closed and
A6: A misses B;
for x st x in B ex W,V being Subset of T st W is open & V is open & A
c= W & x in V & W misses V
proof
let x;
assume x in B;
then not x in A by A6,XBOOLE_0:3;
then
A7: x in A` by SUBSET_1:29;
T is regular by A1,A2,Th24;
then consider V,W being Subset of T such that
A8: V is open & W is open & x in V & A c= W & V misses W by A3,A4,A7;
take W,V;
thus thesis by A8;
end;
then consider Y,Z being Subset of T such that
A9: Y is open & Z is open & A c= Y & B c= Z & Y misses Z by A2,A5,Th23;
take Y,Z;
thus thesis by A9;
end;
hence thesis;
end;
:: Topological space of metric space
reserve x,y,z for Element of PM;
reserve V,W,Y for Subset of PM;
definition
let PM;
func Family_open_set(PM) -> Subset-Family of PM means
:Def4:
for V holds V in it iff for x st x in V holds ex r st r>0 & Ball(x,r) c= V;
existence
proof
defpred P[set] means for x st x in $1 holds ex r st r>0 & Ball(x,r) c= $1;
thus ex S be Subset-Family of PM st for V holds V in S iff P[V] from
SUBSET_1:sch 3;
end;
uniqueness
proof
let FX,GX be Subset-Family of PM;
assume
A1: for V holds V in FX iff for x st x in V holds ex r st r>0 & Ball(x
,r) c= V;
assume
A2: for W holds W in GX iff for y st y in W holds ex p st p>0 & Ball(y
,p) c= W;
for Y holds Y in FX iff Y in GX
proof
let Y;
A3: now
assume Y in GX;
then for x st x in Y holds ex r st r>0 & Ball(x,r) c= Y by A2;
hence Y in FX by A1;
end;
now
assume Y in FX;
then for x st x in Y holds ex r st r>0 & Ball(x,r) c= Y by A1;
hence Y in GX by A2;
end;
hence thesis by A3;
end;
hence thesis by SETFAM_1:31;
end;
end;
theorem Th26:
for x ex r st r>0 & Ball(x,r) c= the carrier of PM
proof
let x;
consider r such that
A1: r = 1;
take r;
thus r > 0 by A1;
thus thesis;
end;
theorem Th27:
for r being Real st PM is triangle & y in Ball(x,r) holds
ex p st p>0 & Ball(y,p) c= Ball(x,r)
proof
let r be Real;
reconsider r9=r as Real;
assume
A1: PM is triangle;
assume
A2: y in Ball(x,r);
then
A3: dist(x,y) < r by METRIC_1:11;
A4: PM is non empty by A2;
thus thesis
proof
set p = r9 - dist(x,y);
take p;
thus p > 0 by A3,XREAL_1:50;
for z holds z in Ball(y,p) implies z in Ball(x,r)
proof
let z;
assume z in Ball(y,p);
then dist(y,z) < r9 - dist(x,y) by METRIC_1:11;
then
A5: dist(x,y) + dist(y,z) < r by XREAL_1:20;
dist(x,y) + dist(y,z) >= dist(x,z) by A1,METRIC_1:4;
then dist(x,z) < r by A5,XXREAL_0:2;
hence thesis by A4,METRIC_1:11;
end;
hence thesis;
end;
end;
theorem
PM is triangle & y in Ball(x,r) /\ Ball(z,p) implies ex q st Ball(y,q)
c= Ball(x,r) & Ball(y,q) c= Ball(z,p)
proof
assume
A1: PM is triangle;
assume
A2: y in Ball(x,r) /\ Ball(z,p);
then y in Ball(x,r) by XBOOLE_0:def 4;
then consider s such that
s > 0 and
A3: Ball(y,s) c= Ball(x,r) by A1,Th27;
y in Ball(z,p) by A2,XBOOLE_0:def 4;
then consider t such that
t > 0 and
A4: Ball(y,t) c= Ball(z,p) by A1,Th27;
take q = min(s,t);
Ball(y,q) c= Ball(y,s) by Th1,XXREAL_0:17;
hence Ball(y,q) c= Ball(x,r) by A3;
Ball(y,q) c= Ball(y,t) by Th1,XXREAL_0:17;
hence thesis by A4;
end;
theorem Th29:
for r being Real st PM is triangle holds Ball(x,r) in
Family_open_set(PM)
proof
let r be Real;
assume PM is triangle;
then
for y st y in Ball(x,r) holds ex p st p>0 & Ball(y,p) c= Ball(x,r) by Th27;
hence thesis by Def4;
end;
theorem Th30:
the carrier of PM in Family_open_set(PM)
proof
the carrier of PM c= the carrier of PM & for y st y in the carrier of PM
holds ex p st p>0 & Ball(y,p) c= the carrier of PM by Th26;
hence thesis by Def4;
end;
theorem Th31:
for V,W st V in Family_open_set(PM) & W in Family_open_set(PM)
holds V /\ W in Family_open_set(PM)
proof
let V,W;
assume that
A1: V in Family_open_set(PM) and
A2: W in Family_open_set(PM);
for z st z in V /\ W ex q st q>0 & Ball(z,q) c= V /\ W
proof
let z;
assume
A3: z in V /\ W;
then z in V by XBOOLE_0:def 4;
then consider p such that
A4: p > 0 and
A5: Ball(z,p) c= V by A1,Def4;
z in W by A3,XBOOLE_0:def 4;
then consider r such that
A6: r > 0 and
A7: Ball(z,r) c= W by A2,Def4;
take q = min(p,r);
thus q > 0 by A4,A6,XXREAL_0:15;
Ball(z,q) c= Ball(z,r) by Th1,XXREAL_0:17;
then
A8: Ball(z,q) c= W by A7;
Ball(z,q) c= Ball(z,p) by Th1,XXREAL_0:17;
then Ball(z,q) c= V by A5;
hence thesis by A8,XBOOLE_1:19;
end;
hence thesis by Def4;
end;
theorem Th32:
for A being Subset-Family of PM st A c= Family_open_set(PM)
holds union A in Family_open_set(PM)
proof
let A be Subset-Family of PM;
assume
A1: A c= Family_open_set(PM);
for x st x in union A ex r st r>0 & Ball(x,r) c= union A
proof
let x;
assume x in union A;
then consider W being set such that
A2: x in W and
A3: W in A by TARSKI:def 4;
reconsider W as Subset of PM by A3;
consider r such that
A4: r>0 and
A5: Ball(x,r) c= W by A1,A2,A3,Def4;
take r;
thus r > 0 by A4;
W c= union A by A3,ZFMISC_1:74;
hence thesis by A5;
end;
hence thesis by Def4;
end;
theorem Th33:
TopStruct (#the carrier of PM,Family_open_set(PM)#) is TopSpace
proof
set T = TopStruct (#the carrier of PM,Family_open_set(PM)#);
A1: for p,q being Subset of T st p in the topology of T & q in the topology
of T holds p /\ q in the topology of T by Th31;
the carrier of T in the topology of T & for a being Subset-Family of T
st a c= the topology of T holds union a in the topology of T by Th30,Th32;
hence thesis by A1,PRE_TOPC:def 1;
end;
definition
let PM;
func TopSpaceMetr PM -> TopStruct equals
TopStruct (#the carrier of PM,
Family_open_set(PM)#);
coherence;
end;
registration
let PM;
cluster TopSpaceMetr PM -> strict TopSpace-like;
coherence by Th33;
end;
registration
let PM be non empty MetrStruct;
cluster TopSpaceMetr PM -> non empty;
coherence;
end;
theorem Th34:
for PM being non empty MetrSpace holds TopSpaceMetr PM is T_2
proof
let PM be non empty MetrSpace;
set TPS = TopSpaceMetr PM;
for x,y being Element of TPS st not x = y ex W,V being Subset of TPS st
W is open & V is open & x in W & y in V & W misses V
proof
let x,y be Element of TPS;
assume
A1: not x = y;
reconsider x,y as Element of PM;
set r = dist(x,y)/2;
dist(x,y) <> 0 by A1,METRIC_1:2;
then dist(x,y) > 0 by METRIC_1:5;
then
A2: r > 0 by XREAL_1:139;
ex W,V being Subset of TPS st W is open & V is open & x in W & y in V
& W misses V
proof
set V = Ball(y,r);
set W = Ball(x,r);
A3: W in Family_open_set(PM) & V in Family_open_set(PM) by Th29;
reconsider W,V as Subset of TPS;
A4: for z being object holds not z in W /\ V
proof
let z be object;
assume
A5: z in W /\ V;
then reconsider z as Element of PM;
z in V by A5,XBOOLE_0:def 4;
then
A6: dist(y,z) < r by METRIC_1:11;
z in W by A5,XBOOLE_0:def 4;
then dist(x,z) < r by METRIC_1:11;
then dist(x,z) + dist(y,z) < r + r by A6,XREAL_1:8;
hence thesis by METRIC_1:4;
end;
take W, V;
dist(x,x) = 0 & dist(y,y) = 0 by METRIC_1:1;
hence thesis by A2,A3,A4,METRIC_1:11,PRE_TOPC:def 2,XBOOLE_0:4;
end;
hence thesis;
end;
hence thesis by PRE_TOPC:def 10;
end;
registration
cluster T_2 non empty strict for TopSpace;
existence
proof
set M = the non empty MetrSpace;
take TopSpaceMetr M;
thus thesis by Th34;
end;
end;
:: Metric on a set
definition
let D be set,f be Function of [:D,D:],REAL;
pred f is_metric_of D means
for a,b,c be Element of D holds (f.(a,b)
= 0 iff a=b) & f.(a,b) = f.(b,a) & f.(a,c)<=f.(a,b)+f.(b,c);
end;
theorem Th35:
for D being set,f being Function of [:D,D:],REAL holds f
is_metric_of D iff MetrStruct (#D,f#) is MetrSpace
proof
let D be set,f be Function of [:D,D:],REAL;
set DF = MetrStruct (#D,f#);
A1: DF is MetrSpace implies f is_metric_of D
proof
assume DF is MetrSpace;
then reconsider DF as MetrSpace;
for a,b,c be Element of DF holds ((the distance of DF).(a,b) = 0 iff
a=b) & (the distance of DF).(a,b) = (the distance of DF).(b,a) & (the distance
of DF).(a,c)<= (the distance of DF).(a,b)+ (the distance of DF).(b,c)
proof
let a,b,c be Element of DF;
A2: (the distance of DF).(a,b) = dist(a,b) by METRIC_1:def 1;
hence (the distance of DF).(a,b) = 0 iff a=b by METRIC_1:1,2;
(the distance of DF).(b,a) = dist(b,a) by METRIC_1:def 1;
hence (the distance of DF).(a,b) = (the distance of DF).(b,a) by A2;
(the distance of DF).(a,c) = dist(a,c) & (the distance of DF).(b,c)
= dist(b,c) by METRIC_1:def 1;
hence thesis by A2,METRIC_1:4;
end;
hence thesis;
end;
f is_metric_of D implies DF is MetrSpace
proof
assume
A3: f is_metric_of D;
for a,b,c be Element of DF holds (dist(a,b) = 0 iff a=b) & dist(a,b) =
dist(b,a) & dist(a,c)<=dist(a,b)+dist(b,c)
proof
let a,b,c be Element of DF;
A4: (the distance of DF).(a,b) = dist(a,b) by METRIC_1:def 1;
hence dist(a,b) = 0 iff a=b by A3;
(the distance of DF).(b,a) = dist(b,a) by METRIC_1:def 1;
hence dist(a,b) = dist(b,a) by A3,A4;
(the distance of DF).(a,c) = dist(a,c) & (the distance of DF).(b,c)
= dist(b,c) by METRIC_1:def 1;
hence thesis by A3,A4;
end;
hence thesis by METRIC_1:6;
end;
hence thesis by A1;
end;
definition
let D be set, f be Function of [:D,D:],REAL;
assume
A1: f is_metric_of D;
func SpaceMetr(D,f) -> strict MetrSpace equals
:Def7:
MetrStruct(#D,f#);
coherence by A1,Th35;
end;
:: Metrizable topological spaces
definition
let IT be TopStruct;
attr IT is metrizable means
ex f being Function of [:the carrier of IT,the
carrier of IT:],REAL st f is_metric_of (the carrier of IT) & Family_open_set(
SpaceMetr (the carrier of IT,f) ) = the topology of IT;
end;
registration
cluster strict metrizable for non empty TopSpace;
existence
proof
set MS = the strict non empty MetrSpace;
take TS = TopSpaceMetr MS;
reconsider f = the distance of MS as Function of [:the carrier of TS,the
carrier of TS:],REAL;
thus TS is strict;
take f;
thus f is_metric_of the carrier of TS by Th35;
hence thesis by Def7;
end;
end;
theorem
for D be non empty set, f be Function of [:D,D:],REAL st f
is_metric_of D holds SpaceMetr(D,f) is non empty
proof
let D be non empty set, f be Function of [:D,D:], REAL;
assume f is_metric_of D;
then SpaceMetr(D,f) = MetrStruct(#D,f#) by Def7;
hence thesis;
end;