:: Metric Spaces as Topological Spaces - Fundamental Concepts
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 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, REAL_1, XBOOLE_0, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI,
SUBSET_1, RCOMP_1, RELAT_1, CONNSP_2, TOPS_1, FUNCT_1, ORDINAL2,
METRIC_1, CARD_1, XXREAL_0, ARYTM_3, REALSET1, ZFMISC_1, XXREAL_1,
COMPLEX1, ARYTM_1, PCOMPS_1, FINSET_1, BORSUK_1, TOPMETR, MEMBERED,
FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED,
XCMPLX_0, XREAL_0, REAL_1, NAT_1, DOMAIN_1, RELAT_1, REALSET1, FUNCT_1,
PARTFUN1, RELSET_1, XXREAL_0, FUNCT_2, FINSET_1, BINOP_1, STRUCT_0,
METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, PCOMPS_1, CONNSP_2,
RCOMP_1, BORSUK_1, COMPLEX1;
constructors SETFAM_1, REAL_1, COMPLEX1, RCOMP_1, REALSET1, TOPS_1, TOPS_2,
COMPTS_1, BORSUK_1, FINSET_1, MEMBERED, XXREAL_2, PCOMPS_1, BINOP_1,
BINOP_2, VALUED_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, REALSET1,
STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, METRIC_3, PCOMPS_1, XXREAL_2,
BORSUK_1, BINOP_2, VALUED_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions PRE_TOPC, TARSKI, TOPS_2, MEMBERED;
equalities STRUCT_0, BINOP_1, REALSET1, PCOMPS_1, METRIC_1;
expansions PRE_TOPC, TARSKI, TOPS_2;
theorems ABSVALUE, BINOP_1, BORSUK_1, COMPTS_1, CONNSP_2, FINSET_1, FUNCT_1,
FUNCT_2, METRIC_1, PCOMPS_1, PRE_TOPC, TARSKI, TOPS_1, TOPS_2, ZFMISC_1,
TBSP_1, RELAT_1, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1,
XREAL_1, COMPLEX1, XXREAL_0, SETFAM_1, XXREAL_1, XXREAL_2;
schemes FUNCT_2;
begin
reserve r for Real;
reserve a, b for Real;
reserve T for non empty TopSpace;
:: Topological spaces
theorem
for T being TopStruct, F being Subset-Family of T holds F is Cover of
T iff the carrier of T c= union F by SETFAM_1:def 11;
reserve A for non empty SubSpace of T;
theorem
T is T_2 implies A is T_2
proof
assume
A1: T is T_2;
for p,q being Point of A st not p = q ex W,V being Subset of A st W is
open & V is open & p in W & q in V & W misses V
proof
let p,q be Point of A such that
A2: not p = q;
reconsider p9 = p, q9 = q as Point of T by PRE_TOPC:25;
consider W,V being Subset of T such that
A3: W is open and
A4: V is open and
A5: p9 in W & q9 in V and
A6: W misses V by A1,A2;
reconsider W9 = W /\ [#] A, V9 = V /\ [#] A as Subset of A;
V in the topology of T by A4;
then
A7: V9 in the topology of A by PRE_TOPC:def 4;
take W9, V9;
W in the topology of T by A3;
then W9 in the topology of A by PRE_TOPC:def 4;
hence W9 is open & V9 is open by A7;
thus p in W9 & q in V9 by A5,XBOOLE_0:def 4;
A8: W /\ V = {} by A6,XBOOLE_0:def 7;
W9 /\ V9 = W /\ (V /\ [#] A) /\ [#] A by XBOOLE_1:16
.= {} /\ [#] A by A8,XBOOLE_1:16
.= {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis;
end;
theorem Th3:
for T being TopSpace, A,B being SubSpace of T st the carrier of A
c= the carrier of B holds A is SubSpace of B
proof
let T be TopSpace, A,B be SubSpace of T;
assume
A1: the carrier of A c= the carrier of B;
A2: for P being Subset of A holds P in the topology of A iff ex Q being
Subset of B st Q in the topology of B & P = Q /\ [#] A
proof
let P be Subset of A;
thus P in the topology of A implies ex Q being Subset of B st Q in the
topology of B & P = Q /\ [#] A
proof
assume P in the topology of A;
then consider Q9 being Subset of T such that
A3: Q9 in the topology of T and
A4: P = Q9 /\ [#] A by PRE_TOPC:def 4;
reconsider Q = Q9 /\ [#] B as Subset of B;
A5: Q in the topology of B by A3,PRE_TOPC:def 4;
P = Q9 /\ ([#] B /\ [#] A) by A1,A4,XBOOLE_1:28
.= Q /\ [#] A by XBOOLE_1:16;
hence thesis by A5;
end;
given Q being Subset of B such that
A6: Q in the topology of B and
A7: P = Q /\ [#] A;
consider P9 being Subset of T such that
A8: P9 in the topology of T and
A9: Q = P9 /\ [#] B by A6,PRE_TOPC:def 4;
P = P9 /\ ([#] B /\ [#] A) by A7,A9,XBOOLE_1:16
.= P9 /\ [#] A by A1,XBOOLE_1:28;
hence thesis by A8,PRE_TOPC:def 4;
end;
the carrier of A c= [#] B by A1;
hence thesis by A2,PRE_TOPC:def 4;
end;
reserve P,Q for Subset of T,
p for Point of T;
theorem Th4:
T|P is SubSpace of T|(P \/ Q) & T|Q is SubSpace of T|(P \/ Q)
proof
[#](T|P) = P & [#](T|(P \/ Q)) = P \/ Q by PRE_TOPC:def 5;
hence T|P is SubSpace of T|(P \/ Q) by Th3,XBOOLE_1:7;
[#](T|Q) = Q & [#](T|(P \/ Q)) = P \/ Q by PRE_TOPC:def 5;
hence thesis by Th3,XBOOLE_1:7;
end;
theorem
for P being non empty Subset of T st p in P for Q being a_neighborhood
of p holds for p9 being Point of T|P, Q9 being Subset of T|P st Q9 = Q /\ P &
p9= p holds Q9 is a_neighborhood of p9
proof
let P be non empty Subset of T;
assume
A1: p in P;
let Q be a_neighborhood of p;
let p9 be Point of T|P, Q9 be Subset of T|P such that
A2: Q9 = Q /\ P and
A3: p9= p;
p in Int Q by CONNSP_2:def 1;
then consider S being Subset of T such that
A4: S is open and
A5: S c= Q and
A6: p in S by TOPS_1:22;
reconsider R = S /\ P as Subset of T|P by TOPS_2:29;
A7: R c= Q9 by A5,A2,XBOOLE_1:26;
S /\ [#](T|P) = S /\ P by PRE_TOPC:def 5;
then
A8: R is open by A4,TOPS_2:24;
p9 in R by A1,A6,A3,XBOOLE_0:def 4;
then p9 in Int Q9 by A8,A7,TOPS_1:22;
hence thesis by CONNSP_2:def 1;
end;
theorem
for A,B being TopSpace for f being Function of A,B for C being Subset
of B holds f is continuous implies for h being Function of A,B|C st h = f holds
h is continuous
proof
let A,B be TopSpace, f be Function of A,B, C be Subset of B;
assume
A1: f is continuous;
A2: the carrier of B|C = [#](B|C) .= C by PRE_TOPC:def 5;
let h be Function of A,B|C such that
A3: h = f;
A4: rng f c= the carrier of B|C by A3,RELAT_1:def 19;
for P being Subset of B|C holds P is closed implies h"P is closed
proof
let P be Subset of B|C;
assume P is closed;
then consider Q being Subset of B such that
A5: Q is closed and
A6: Q /\ ([#](B|C)) = P by PRE_TOPC:13;
h"P = f"(Q /\ C) by A3,A6,PRE_TOPC:def 5
.= f"Q /\ f"C by FUNCT_1:68
.= f"Q /\ f"(rng f /\ C) by RELAT_1:133
.= f"Q /\ f"(rng f) by A2,A4,XBOOLE_1:28
.= f"Q /\ dom f by RELAT_1:134
.= f"Q by RELAT_1:132,XBOOLE_1:28;
hence thesis by A1,A5;
end;
hence thesis;
end;
theorem
for X being TopStruct, Y being non empty TopStruct, K0 being Subset of
X, f being Function of X,Y, g being Function of X|K0,Y st f is continuous & g =
f|K0 holds g is continuous
proof
let X be TopStruct,Y be non empty TopStruct, K0 be Subset of X, f be
Function of X,Y,g be Function of X|K0,Y;
assume that
A1: f is continuous and
A2: g=f|K0;
A3: [#]Y <> {};
for G being Subset of Y st G is open holds g"G is open
proof
let G be Subset of Y;
[#](X|K0)=K0 by PRE_TOPC:def 5;
then
A4: g"G= [#](X|K0) /\ f"G by A2,FUNCT_1:70;
assume G is open;
then f"G is open by A3,A1,TOPS_2:43;
hence thesis by A4,TOPS_2:24;
end;
hence thesis by A3,TOPS_2:43;
end;
:: Some definitions & theorems about metrical spaces
reserve M for non empty MetrSpace,
p for Point of M;
Lm1: for M be MetrSpace holds MetrStruct (#the carrier of M, the distance of M
#) is MetrSpace
proof
let M be MetrSpace;
now
let a,b,c be Element of MetrStruct (#the carrier of M, the
distance of M#);
reconsider a9=a, b9=b, c9=c as Element of M;
A1: dist(a,c) = (the distance of M).(a,c)
.= dist(a9,c9);
A2: dist(a,b) = (the distance of M).(a,b)
.= dist(a9,b9);
hence dist(a,b) = 0 iff a=b by METRIC_1:1,2;
dist(b,a) = (the distance of M).(b,a)
.= dist(b9,a9);
hence dist(a,b) = dist(b,a) by A2;
dist(b,c) = (the distance of M).(b,c)
.= dist(b9,c9);
hence dist(a,c)<=dist(a,b)+dist(b,c) by A2,A1,METRIC_1:4;
end;
hence thesis by METRIC_1:6;
end;
definition
let M be MetrSpace;
mode SubSpace of M -> MetrSpace means
:Def1:
the carrier of it c= the
carrier of M & for x,y being Point of it holds (the distance of it).(x,y) = (
the distance of M).(x,y);
existence
proof
reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as
MetrSpace by Lm1;
take MM;
thus the carrier of MM c= the carrier of M;
let x,y be Point of MM;
thus thesis;
end;
end;
registration
let M be MetrSpace;
cluster strict for SubSpace of M;
existence
proof
reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as
MetrSpace by Lm1;
for x,y being Point of MM holds (the distance of MM).(x,y) = (the
distance of M).(x,y);
then MM is SubSpace of M by Def1;
hence thesis;
end;
end;
registration
let M be non empty MetrSpace;
cluster strict non empty for SubSpace of M;
existence
proof
reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as
MetrSpace by Lm1;
for x,y being Point of MM holds (the distance of MM).(x,y) = (the
distance of M).(x,y);
then MM is SubSpace of M by Def1;
hence thesis;
end;
end;
reserve A for non empty SubSpace of M;
theorem Th8:
for p being Point of A holds p is Point of M
proof
let p be Point of A;
p in the carrier of A & the carrier of A c= the carrier of M by Def1;
hence thesis;
end;
theorem Th9:
for r being Real for M being MetrSpace, A being SubSpace
of M for x being Point of M, x9 being Point of A st x = x9 holds Ball(x9,r) =
Ball(x,r) /\ the carrier of A
proof
let r be Real;
let M be MetrSpace, A be SubSpace of M;
let x be Point of M, x9 be Point of A;
assume
A1: x = x9;
now
let a be object;
assume
A2: a in Ball(x9,r);
then reconsider y9 = a as Point of A;
the carrier of A c= the carrier of M by Def1;
then
A3: M is non empty by A2;
A is non empty by A2;
then reconsider y = y9 as Point of M by A3,Th8;
dist(x9,y9) < r by A2,METRIC_1:11;
then (the distance of A).(x9,y9) < r;
then (the distance of M).(x,y) < r by A1,Def1;
then dist(x,y) < r;
then a in Ball(x,r) by A3,METRIC_1:11;
hence a in Ball(x,r) /\ the carrier of A by A2,XBOOLE_0:def 4;
end;
then
A4: Ball(x9,r) c= Ball(x,r) /\ the carrier of A;
now
let a be object;
assume
A5: a in Ball(x,r) /\ the carrier of A;
then reconsider y9 = a as Point of A by XBOOLE_0:def 4;
reconsider y = y9 as Point of M by A5;
a in Ball(x,r) by A5,XBOOLE_0:def 4;
then dist(x,y) < r by METRIC_1:11;
then (the distance of M).(x,y) < r;
then (the distance of A).(x9,y9) < r by A1,Def1;
then
A6: dist(x9,y9) < r;
the carrier of A is non empty by A5;
then A is non empty;
hence a in Ball(x9,r) by A6,METRIC_1:11;
end;
then Ball(x,r) /\ the carrier of A c= Ball(x9,r);
hence thesis by A4,XBOOLE_0:def 10;
end;
definition
let M be non empty MetrSpace, A be non empty Subset of M;
func M|A -> strict SubSpace of M means
:Def2:
the carrier of it = A;
existence
proof
reconsider B=A as non empty set;
set d = (the distance of M)||A;
A1: dom d = dom (the distance of M) /\ [:A,A:] by RELAT_1:61
.= [:the carrier of M,the carrier of M:] /\ [:A,A:] by FUNCT_2:def 1
.= [: (the carrier of M) /\ A, (the carrier of M) /\ A:] by ZFMISC_1:100
.= [: (the carrier of M) /\ A, A:] by XBOOLE_1:28
.= [: A, A :] by XBOOLE_1:28;
rng d c= REAL by RELAT_1:def 19;
then reconsider d as Function of [:B,B:],REAL by A1,FUNCT_2:def 1
,RELSET_1:4;
set MM = MetrStruct (# B, d #);
A2: now
let a,b be Element of MM;
thus dist(a,b) = (the distance of MM).(a,b)
.= (the distance of M) . [a,b] by A1,FUNCT_1:47
.= (the distance of M).(a,b);
end;
now
let a,b,c be Element of MM;
reconsider a9=a, b9=b, c9=c as Point of M by TARSKI:def 3;
A3: dist(a,c) = (the distance of M).(a,c) by A2
.= dist(a9,c9);
dist(a,b) = (the distance of M).(a,b) by A2
.= dist(a9,b9);
hence dist(a,b) = 0 iff a=b by METRIC_1:1,2;
A4: dist(b,c) = (the distance of M).(b,c) by A2
.= dist(b9,c9);
thus dist(a,b) = (the distance of M).(a9,b9) by A2
.= dist(b9,a9) by METRIC_1:def 1
.= (the distance of M).(b9,a9)
.= dist(b,a) by A2;
dist(a,b) = (the distance of M).(a,b) by A2
.= dist(a9,b9);
hence dist(a,c)<=dist(a,b)+dist(b,c) by A3,A4,METRIC_1:4;
end;
then reconsider MM as MetrSpace by METRIC_1:6;
now
let x, y be Point of MM;
thus (the distance of MM).(x,y) = dist(x,y)
.= (the distance of M).(x,y) by A2;
end;
then reconsider MM as strict SubSpace of M by Def1;
take MM;
thus thesis;
end;
uniqueness
proof
let S1,S2 be strict SubSpace of M;
assume that
A5: the carrier of S1 = A and
A6: the carrier of S2 = A;
now
let a,b be Element of A;
thus (the distance of S1).(a,b) = (the distance of M).(a,b) by A5,Def1
.= (the distance of S2).(a,b) by A6,Def1;
end;
hence thesis by A5,A6,BINOP_1:2;
end;
end;
registration
let M be non empty MetrSpace, A be non empty Subset of M;
cluster M|A -> non empty;
coherence by Def2;
end;
definition
let a,b be Real;
assume
A1: a <= b;
func Closed-Interval-MSpace(a,b) -> strict non empty SubSpace of RealSpace
means
:Def3:
for P being non empty Subset of RealSpace st P = [. a,b .] holds
it = RealSpace | P;
existence
proof
reconsider P = [. a,b .] as Subset of RealSpace;
reconsider P as non empty Subset of RealSpace by A1,XXREAL_1:1;
take RealSpace | P;
thus thesis;
end;
uniqueness
proof
reconsider P = [. a,b .] as Subset of RealSpace;
reconsider P as non empty Subset of RealSpace by A1,XXREAL_1:1;
let S1,S2 be strict non empty SubSpace of RealSpace;
assume that
A2: for P being non empty Subset of RealSpace st P = [. a,b .] holds
S1 = RealSpace | P and
A3: for P being non empty Subset of RealSpace st P = [. a,b .] holds
S2 = RealSpace | P;
thus S1 = RealSpace | P by A2
.= S2 by A3;
end;
end;
theorem Th10:
a <= b implies the carrier of Closed-Interval-MSpace(a,b) = [. a ,b .]
proof
assume
A1: a <= b;
then reconsider P = [. a,b .] as non empty Subset of RealSpace by XXREAL_1:1;
thus the carrier of Closed-Interval-MSpace(a,b) = the carrier of RealSpace |
P by A1,Def3
.= [. a,b .] by Def2;
end;
reserve F,G for Subset-Family of M;
definition
let M be MetrStruct, F be Subset-Family of M;
attr F is being_ball-family means
for P being set holds P in F
implies ex p being Point of M, r st P = Ball(p,r);
end;
theorem Th11:
for p,q being Point of RealSpace, x,y being Real holds x=
p & y=q implies dist(p,q) = |.x-y.|
by METRIC_1:def 12;
:: Metric spaces and topology
theorem
for M being MetrStruct holds the carrier of M = the carrier of
TopSpaceMetr M & the topology of TopSpaceMetr M = Family_open_set M;
theorem Th13:
TopSpaceMetr(A) is SubSpace of TopSpaceMetr(M)
proof
set T = TopSpaceMetr M, R = TopSpaceMetr A;
thus [#](R) c= [#](T) by Def1;
let P be Subset of R;
thus P in the topology of R implies ex Q being Subset of T st Q in the
topology of T & P = Q /\ [#](R)
proof
set QQ = {Ball(x,r) where x is Point of M, r is Real:
x in P & r > 0 & Ball(x,r) /\ the carrier of A c= P};
for X being set st X in QQ holds X c= the carrier of M
proof
let X be set;
assume X in QQ;
then
ex x being Point of M, r being Real
st X = Ball(x,r) & x in P & r > 0 & Ball(x,r) /\ the carrier of A c= P;
hence thesis;
end;
then reconsider Q = union QQ as Subset of M by ZFMISC_1:76;
reconsider Q9 = Q as Subset of T;
assume P in the topology of R;
then
A1: P in Family_open_set A;
A2: P c= Q9 /\ [#](R)
proof
reconsider P9 = P as Subset of A;
let a be object;
assume
A3: a in P;
then reconsider x = a as Point of A;
reconsider x9 = x as Point of M by Th8;
consider r such that
A4: r > 0 and
A5: Ball(x,r) c= P9 by A1,A3,PCOMPS_1:def 4;
Ball(x,r) = Ball(x9,r) /\ the carrier of A by Th9;
then
A6: Ball(x9,r) in QQ by A3,A4,A5;
x9 in Ball(x9,r) by A4,TBSP_1:11;
then a in Q9 by A6,TARSKI:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
take Q9;
for x being Point of M st x in Q ex r st r > 0 & Ball(x,r) c= Q
proof
let x be Point of M;
assume x in Q;
then consider Y being set such that
A7: x in Y and
A8: Y in QQ by TARSKI:def 4;
consider x9 being Point of M, r being Real such that
A9: Y = Ball(x9,r) and
x9 in P and
r > 0 and
Ball(x9,r) /\ the carrier of A c= P by A8;
consider p being Real such that
A10: p > 0 and
A11: Ball(x,p) c= Ball(x9,r) by A7,A9,PCOMPS_1:27;
take p;
thus p > 0 by A10;
Y c= Q by A8,ZFMISC_1:74;
hence thesis by A9,A11;
end;
then Q in Family_open_set M by PCOMPS_1:def 4;
hence Q9 in the topology of T;
Q9 /\ [#](R) c= P
proof
let a be object;
assume
A12: a in Q9 /\ [#](R);
then a in Q9 by XBOOLE_0:def 4;
then consider Y being set such that
A13: a in Y and
A14: Y in QQ by TARSKI:def 4;
consider x being Point of M, r being Real such that
A15: Y = Ball(x,r) and
x in P and
r > 0 and
A16: Ball(x,r) /\ the carrier of A c= P by A14;
a in Ball(x,r) /\ the carrier of A by A12,A13,A15,XBOOLE_0:def 4;
hence thesis by A16;
end;
hence P = Q9 /\ [#](R) by A2,XBOOLE_0:def 10;
end;
reconsider P9 = P as Subset of A;
given Q being Subset of T such that
A17: Q in the topology of T and
A18: P = Q /\ [#](R);
reconsider Q9 = Q as Subset of M;
for p being Point of A st p in P9 ex r st r>0 & Ball(p,r) c= P9
proof
let p be Point of A;
reconsider p9 = p as Point of M by Th8;
assume p in P9;
then
A19: p9 in Q9 by A18,XBOOLE_0:def 4;
Q9 in Family_open_set M by A17;
then consider r such that
A20: r>0 and
A21: Ball(p9,r) c= Q9 by A19,PCOMPS_1:def 4;
Ball(p,r) = Ball(p9,r) /\ the carrier of A by Th9;
then Ball(p,r) c= Q /\ the carrier of A by A21,XBOOLE_1:26;
then Ball(p,r) c= Q /\ the carrier of R;
hence thesis by A18,A20;
end;
then P in Family_open_set A by PCOMPS_1:def 4;
hence thesis;
end;
theorem Th14:
for r being Real for M being triangle MetrStruct, p being
Point of M for P being Subset of TopSpaceMetr(M) st P = Ball(p,r) holds P is
open
by PCOMPS_1:29;
theorem Th15:
for P being Subset of TopSpaceMetr(M) holds P is open iff for p
being Point of M st p in P ex r being Real st r>0 & Ball(p,r) c= P
by PCOMPS_1:def 4;
definition
let M be MetrStruct;
attr M is compact means
TopSpaceMetr(M) is compact;
end;
theorem
M is compact iff for F st F is being_ball-family & F is Cover of M ex
G st G c= F & G is Cover of M & G is finite
proof
thus M is compact implies for F st F is being_ball-family & F is Cover of M
ex G st G c= F & G is Cover of M & G is finite
proof
set TM = TopSpaceMetr(M);
assume M is compact;
then
A1: TopSpaceMetr(M) is compact;
let F;
reconsider TF = F as Subset-Family of TM;
assume that
A2: F is being_ball-family and
A3: F is Cover of M;
A4: TF is open
proof
let P be Subset of TM;
reconsider P9 = P as Subset of M;
assume P in TF;
then ex p,r st P9 = Ball(p,r) by A2;
hence thesis by Th14;
end;
the carrier of M c= union F by A3,SETFAM_1:def 11;
then the carrier of TM c= union TF;
then TF is Cover of TM by SETFAM_1:def 11;
then consider TG being Subset-Family of TM such that
A5: TG c= TF and
A6: TG is Cover of TM and
A7: TG is finite by A1,A4,COMPTS_1:def 1;
reconsider G = TG as Subset-Family of M;
take G;
the carrier of TM c= union TG by A6,SETFAM_1:def 11;
then the carrier of M c= union G;
hence thesis by A5,A7,SETFAM_1:def 11;
end;
thus (for F st F is being_ball-family & F is Cover of M ex G st G c= F & G
is Cover of M & G is finite) implies M is compact
proof
set TM = TopSpaceMetr(M);
assume
A8: for F st F is being_ball-family & F is Cover of M ex G st G c= F
& G is Cover of M & G is finite;
now
let F be Subset-Family of TM;
set Z = { Ball(p,r) where p is Point of M, r is Real: ex P being Subset
of TM st P in F & Ball(p,r) c= P};
Z c= bool the carrier of M
proof
let a be object;
assume a in Z;
then
ex p being Point of M, r being Real st a = Ball(p,r) & ex P being
Subset of TM st P in F & Ball(p,r) c= P;
hence thesis;
end;
then reconsider Z as Subset-Family of M;
assume that
A9: F is Cover of TM and
A10: F is open;
the carrier of M c= union Z
proof
let a be object;
assume a in the carrier of M;
then reconsider p = a as Point of M;
the carrier of TM c= union F & the carrier of TM = the carrier of
M by A9,SETFAM_1:def 11;
then p in union F;
then consider P being set such that
A11: p in P and
A12: P in F by TARSKI:def 4;
reconsider P as Subset of TM by A12;
P is open by A10,A12;
then consider r being Real such that
A13: r>0 and
A14: Ball(p,r) c= P by A11,Th15;
reconsider r9 = r as Element of REAL by XREAL_0:def 1;
A15: a in Ball(p,r) by A13,TBSP_1:11;
Ball(p,r9) in Z by A12,A14;
hence thesis by A15,TARSKI:def 4;
end;
then
A16: Z is Cover of M by SETFAM_1:def 11;
reconsider F9 = F as non empty Subset-Family of TM by A9,TOPS_2:3;
defpred X[object,object] means
ex D1,D2 being set st D1 = $1 & D2 = $2 & D1 c= D2;
Z is being_ball-family
proof
let P be set;
assume P in Z;
then
ex p being Point of M, r being Real st P = Ball(p,r) & ex P being
Subset of TM st P in F & Ball(p,r) c= P;
hence thesis;
end;
then consider G being Subset-Family of M such that
A17: G c= Z and
A18: G is Cover of M and
A19: G is finite by A8,A16;
A20: for a being object st a in G ex u being object st u in F9 & X[a,u]
proof
let a be object;
assume a in G;
then a in Z by A17;
then consider p being Point of M, r being Real such that
A21: Ball(p,r) = a and
A22: ex P being Subset of TM st P in F & Ball(p,r) c= P;
consider P being Subset of TM such that
A23: P in F & Ball(p,r) c= P by A22;
take P;
thus thesis by A21,A23;
end;
consider f being Function of G,F9 such that
A24: for a being object st a in G holds X[a,f.a] from FUNCT_2:sch 1(A20
);
reconsider GG = rng f as Subset-Family of TM by TOPS_2:2;
take GG;
thus GG c= F;
the carrier of TM c= union GG
proof
A25: the carrier of TM = the carrier of M & the carrier of M c= union
G by A18,SETFAM_1:def 11;
let a be object;
assume a in the carrier of TM;
then consider P being set such that
A26: a in P and
A27: P in G by A25,TARSKI:def 4;
X[P,f.P] by A24,A27;
then
A28: P c= f.P;
dom f = G by FUNCT_2:def 1;
then f.P in GG by A27,FUNCT_1:def 3;
hence thesis by A26,A28,TARSKI:def 4;
end;
hence GG is Cover of TM by SETFAM_1:def 11;
dom f = G by FUNCT_2:def 1;
hence GG is finite by A19,FINSET_1:8;
end;
then TM is compact by COMPTS_1:def 1;
hence thesis;
end;
end;
:: REAL as topological space
definition
func R^1 -> TopSpace equals
TopSpaceMetr(RealSpace);
correctness;
end;
registration
cluster R^1 -> strict non empty;
coherence;
end;
theorem
the carrier of R^1 = REAL;
definition
let a,b be Real;
func Closed-Interval-TSpace(a,b) -> strict non empty SubSpace of R^1 equals
TopSpaceMetr(Closed-Interval-MSpace(a,b));
coherence by Th13;
end;
theorem Th18:
a <= b implies the carrier of Closed-Interval-TSpace(a,b) = [. a,b .]
by Th10;
theorem Th19:
a <= b implies for P being Subset of R^1 st P = [. a,b .] holds
Closed-Interval-TSpace(a,b) = R^1|P
proof
assume
A1: a <= b;
let P be Subset of R^1;
assume P = [. a,b .];
then [#](Closed-Interval-TSpace(a,b)) = P by A1,Th18;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th20:
Closed-Interval-TSpace(0,1) = I[01]
proof
reconsider P = [.0,1.] as Subset of R^1;
set TR = TopSpaceMetr(RealSpace);
reconsider P9 = P as Subset of TR;
thus Closed-Interval-TSpace(0,1) = TR|P9 by Th19
.= I[01] by BORSUK_1:def 13;
end;
definition
redefine func I[01] -> SubSpace of R^1; :: redefines I[01] (BORSUK_1, definition)
coherence by Th20;
end;
Lm2: for r be Real holds r >= 0 & a + r <= b implies a <= b
proof
let r be Real;
assume r >= 0 & a + r <= b;
then a + r - r <= b - r & b - r <= b by XREAL_1:9,43;
hence thesis by XXREAL_0:2;
end;
theorem
for f being Function of R^1,R^1 st ex a,b being Real
st for x being Real holds f.x = a*x + b holds f is continuous
proof
let f be Function of R^1,R^1;
given a,b being Real such that
A1: for x being Real holds f.x = a*x + b;
for W being Point of R^1, G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
let W be Point of R^1, G be a_neighborhood of f.W;
reconsider Y = f.W as Point of RealSpace;
A2: f.W in Int G by CONNSP_2:def 1;
then consider Q being Subset of R^1 such that
A3: Q is open and
A4: Q c= G and
A5: f.W in Q by TOPS_1:22;
consider r being Real such that
A6: r>0 and
A7: Ball(Y,r) c= Q by A3,A5,Th15;
now
per cases;
suppose
A8: a = 0;
set H = [#](R^1);
W in H;
then W in Int H by TOPS_1:23;
then reconsider H as a_neighborhood of W by CONNSP_2:def 1;
for y being object holds y in {b} iff
ex x being object st x in dom f &
x in H & y = f.x
proof
let y be object;
thus y in {b} implies
ex x being object st x in dom f & x in H & y = f.x
proof
assume
A9: y in {b};
take 0;
dom f = the carrier of R^1 by FUNCT_2:def 1;
then In(0,REAL) in dom f & In(0,REAL) in H;
hence 0 in dom f & 0 in H;
thus f.0 = 0 * 0 + b by A1,A8
.= y by A9,TARSKI:def 1;
end;
given x being object such that
A10: x in dom f and
x in H and
A11: y = f.x;
reconsider x as Real by A10;
y = 0 * x + b by A1,A8,A11
.= b;
hence thesis by TARSKI:def 1;
end;
then
A12: f.:H = {b} by FUNCT_1:def 6;
reconsider W9 = W as Real;
A13: Int G c= G by TOPS_1:16;
f.W = 0 * W9 + b by A1,A8
.= b;
then f.:H c= G by A2,A12,A13,ZFMISC_1:31;
hence thesis;
end;
suppose
A14: a <> 0;
reconsider W9 = W as Point of RealSpace;
set d = r/(2* |.a.|);
reconsider H = Ball(W9,d) as Subset of R^1;
H is open by Th14;
then
A15: Int H = H by TOPS_1:23;
|.a.| > 0 by A14,COMPLEX1:47;
then 2*|.a.| > 0 by XREAL_1:129;
then W in Int H by A6,A15,TBSP_1:11,XREAL_1:139;
then reconsider H as a_neighborhood of W by CONNSP_2:def 1;
A16: f.:H c= Ball(Y,r)
proof
reconsider W99 = W9 as Real;
let y be object;
reconsider Y9 = Y as Real;
assume y in f.:H;
then consider x being object such that
A17: x in dom f and
A18: x in H and
A19: y = f.x by FUNCT_1:def 6;
reconsider x9=x as Point of RealSpace by A18;
reconsider y9=y as Element of REAL by A17,A19,FUNCT_2:5;
reconsider x99 = x9 as Real;
reconsider yy=y9 as Point of RealSpace;
A20: |.a.| > 0 by A14,COMPLEX1:47;
dist(W9,x9) < d by A18,METRIC_1:11;
then |.W99 - x99.| < d by Th11;
then |.a.|*|.W99 - x99.| < |.a.|*d by A20,XREAL_1:68;
then |.a*(W99 - x99).| < |.a.|*d by COMPLEX1:65;
then |.(a*W99+b) - (a*x99+b).| < |.a.|*d;
then |.Y9 - (a*x99+b).| < |.a.|*d by A1;
then
A21: |.Y9 - y9.| < |.a.|*d by A1,A19;
|.a.| <> 0 by A14,ABSVALUE:2;
then
A22: |.a.|*d = r/2 by XCMPLX_1:92;
r/2+r/2 = r & r/2>=0 by A6,XREAL_1:136;
then |.Y9-y9.| < r by A21,A22,Lm2;
then dist(Y,yy) < r by Th11;
hence thesis by METRIC_1:11;
end;
Ball(Y,r) c= G by A4,A7;
hence thesis by A16,XBOOLE_1:1;
end;
end;
hence thesis;
end;
hence thesis by BORSUK_1:def 1;
end;
::Moved from JORDAN16:6, AK 20.02.2006
theorem
for T being non empty TopSpace, A,B being Subset of T st A c= B holds
T|A is SubSpace of T|B
proof
let T be non empty TopSpace, A,B be Subset of T;
assume A c= B;
then A \/ B = B by XBOOLE_1:12;
hence thesis by Th4;
end;
::Moved from JGRAPH_5:6,7, AK 20.02.2006
theorem Th23:
for a,b,d,e being Real, B being Subset of
Closed-Interval-TSpace(d,e) st d<=a & a<=b & b<=e & B=[.a,b.] holds
Closed-Interval-TSpace(a,b)=Closed-Interval-TSpace(d,e)|B
proof
let a,b,d,e be Real, B be Subset of Closed-Interval-TSpace(d,e);
assume that
A1: d<=a and
A2: a<=b and
A3: b<=e and
A4: B=[.a,b.];
a<=e by A2,A3,XXREAL_0:2;
then
A5: a in [.d,e.] by A1,XXREAL_1:1;
A6: d<=b by A1,A2,XXREAL_0:2;
then reconsider A=[.d,e.] as non empty Subset of R^1 by A3,XXREAL_1:1;
b in [.d,e.] by A3,A6,XXREAL_1:1;
then
A7: [.a,b.] c= [.d,e.] by A5,XXREAL_2:def 12;
reconsider B2=[.a,b.] as non empty Subset of R^1 by A2,XXREAL_1:1;
A8: Closed-Interval-TSpace(a,b)=R^1|B2 by A2,Th19;
Closed-Interval-TSpace(d,e)=R^1|A by A3,A6,Th19,XXREAL_0:2;
hence thesis by A4,A8,A7,PRE_TOPC:7;
end;
theorem
for a,b being Real, B being Subset of I[01] st 0<=a & a<=b & b
<=1 & B=[.a,b.] holds Closed-Interval-TSpace(a,b)=I[01]|B by Th20,Th23;
:: from BORSUK_6, 2007.04.08, A,T.
definition
let T be 1-sorted;
attr T is real-membered means
:Def8:
the carrier of T is real-membered;
end;
registration
cluster I[01] -> real-membered;
coherence
by BORSUK_1:40;
end;
:: from RCOMP_3, 2007.04.08, A,T.
registration
cluster non empty real-membered for 1-sorted;
existence
proof
take I[01];
thus thesis;
end;
end;
registration
let S be real-membered 1-sorted;
cluster the carrier of S -> real-membered;
coherence by Def8;
end;
:: from BORSUK_6, 2010.03.07, A.T.
registration
cluster R^1 -> real-membered;
coherence;
end;
:: from BORSUK_6, 2010.05.31, A.K.
registration
cluster strict non empty real-membered for TopSpace;
existence
proof
take I[01];
thus thesis;
end;
end;
registration
let T be real-membered TopStruct;
cluster -> real-membered for SubSpace of T;
coherence
proof
let R be SubSpace of T;
let x be object;
the carrier of R c= the carrier of T by BORSUK_1:1;
hence thesis;
end;
end;
:: from EUCLID_9, 2010.10.05, A.K.
registration
cluster RealSpace -> real-membered;
coherence;
end;