:: Metric Spaces as Topological Spaces - Fundamental Concepts
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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;
begin
reserve r for Real;
reserve a, b for Real;
reserve T for non empty TopSpace;
:: Topological spaces
theorem :: TOPMETR:1
for T being TopStruct, F being Subset-Family of T holds F is Cover of
T iff the carrier of T c= union F;
reserve A for non empty SubSpace of T;
theorem :: TOPMETR:2
T is T_2 implies A is T_2;
theorem :: TOPMETR:3
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;
reserve P,Q for Subset of T,
p for Point of T;
theorem :: TOPMETR:4
T|P is SubSpace of T|(P \/ Q) & T|Q is SubSpace of T|(P \/ Q);
theorem :: TOPMETR:5
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;
theorem :: TOPMETR:6
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;
theorem :: TOPMETR:7
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;
:: Some definitions & theorems about metrical spaces
reserve M for non empty MetrSpace,
p for Point of M;
definition
let M be MetrSpace;
mode SubSpace of M -> MetrSpace means
:: TOPMETR:def 1
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);
end;
registration
let M be MetrSpace;
cluster strict for SubSpace of M;
end;
registration
let M be non empty MetrSpace;
cluster strict non empty for SubSpace of M;
end;
reserve A for non empty SubSpace of M;
theorem :: TOPMETR:8
for p being Point of A holds p is Point of M;
theorem :: TOPMETR:9
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;
definition
let M be non empty MetrSpace, A be non empty Subset of M;
func M|A -> strict SubSpace of M means
:: TOPMETR:def 2
the carrier of it = A;
end;
registration
let M be non empty MetrSpace, A be non empty Subset of M;
cluster M|A -> non empty;
end;
definition
let a,b be Real;
assume
a <= b;
func Closed-Interval-MSpace(a,b) -> strict non empty SubSpace of RealSpace
means
:: TOPMETR:def 3
for P being non empty Subset of RealSpace st P = [. a,b .] holds
it = RealSpace | P;
end;
theorem :: TOPMETR:10
a <= b implies the carrier of Closed-Interval-MSpace(a,b) = [. a ,b .];
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
:: TOPMETR:def 4
for P being set holds P in F
implies ex p being Point of M, r st P = Ball(p,r);
end;
theorem :: TOPMETR:11
for p,q being Point of RealSpace, x,y being Real holds x=
p & y=q implies dist(p,q) = |.x-y.|;
:: Metric spaces and topology
theorem :: TOPMETR:12
for M being MetrStruct holds the carrier of M = the carrier of
TopSpaceMetr M & the topology of TopSpaceMetr M = Family_open_set M;
theorem :: TOPMETR:13
TopSpaceMetr(A) is SubSpace of TopSpaceMetr(M);
theorem :: TOPMETR:14
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;
theorem :: TOPMETR:15
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;
definition
let M be MetrStruct;
attr M is compact means
:: TOPMETR:def 5
TopSpaceMetr(M) is compact;
end;
theorem :: TOPMETR:16
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;
:: REAL as topological space
definition
func R^1 -> TopSpace equals
:: TOPMETR:def 6
TopSpaceMetr(RealSpace);
end;
registration
cluster R^1 -> strict non empty;
end;
theorem :: TOPMETR:17
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
:: TOPMETR:def 7
TopSpaceMetr(Closed-Interval-MSpace(a,b));
end;
theorem :: TOPMETR:18
a <= b implies the carrier of Closed-Interval-TSpace(a,b) = [. a,b .];
theorem :: TOPMETR:19
a <= b implies for P being Subset of R^1 st P = [. a,b .] holds
Closed-Interval-TSpace(a,b) = R^1|P;
theorem :: TOPMETR:20
Closed-Interval-TSpace(0,1) = I[01];
definition
redefine func I[01] -> SubSpace of R^1;
end;
theorem :: TOPMETR:21
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;
::Moved from JORDAN16:6, AK 20.02.2006
theorem :: TOPMETR:22
for T being non empty TopSpace, A,B being Subset of T st A c= B holds
T|A is SubSpace of T|B;
::Moved from JGRAPH_5:6,7, AK 20.02.2006
theorem :: TOPMETR:23
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;
theorem :: TOPMETR:24
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;
:: from BORSUK_6, 2007.04.08, A,T.
definition
let T be 1-sorted;
attr T is real-membered means
:: TOPMETR:def 8
the carrier of T is real-membered;
end;
registration
cluster I[01] -> real-membered;
end;
:: from RCOMP_3, 2007.04.08, A,T.
registration
cluster non empty real-membered for 1-sorted;
end;
registration
let S be real-membered 1-sorted;
cluster the carrier of S -> real-membered;
end;
:: from BORSUK_6, 2010.03.07, A.T.
registration
cluster R^1 -> real-membered;
end;
:: from BORSUK_6, 2010.05.31, A.K.
registration
cluster strict non empty real-membered for TopSpace;
end;
registration
let T be real-membered TopStruct;
cluster -> real-membered for SubSpace of T;
end;
:: from EUCLID_9, 2010.10.05, A.K.
registration
cluster RealSpace -> real-membered;
end;