let M, N be non empty MetrSpace; :: thesis: ( the carrier of M = the carrier of N & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball n,r1 c= Ball m,r ) ) & ( for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball m,r1 c= Ball n,r ) ) implies TopSpaceMetr M = TopSpaceMetr N )
assume that
A1:
the carrier of M = the carrier of N
and
A2:
for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball n,r1 c= Ball m,r )
and
A3:
for m being Point of M
for n being Point of N
for r being Real st r > 0 & m = n holds
ex r1 being Real st
( r1 > 0 & Ball m,r1 c= Ball n,r )
; :: thesis: TopSpaceMetr M = TopSpaceMetr N
A4:
( TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) & TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) )
by PCOMPS_1:def 6;
Family_open_set M = Family_open_set N
proof
thus
Family_open_set M c= Family_open_set N
:: according to XBOOLE_0:def 10 :: thesis: Family_open_set N c= Family_open_set Mproof
let X be
set ;
:: according to TARSKI:def 3 :: thesis: ( not X in Family_open_set M or X in Family_open_set N )
assume A5:
X in Family_open_set M
;
:: thesis: X in Family_open_set N
for
n being
Point of
N st
n in X holds
ex
r being
Real st
(
r > 0 &
Ball n,
r c= X )
proof
let n be
Point of
N;
:: thesis: ( n in X implies ex r being Real st
( r > 0 & Ball n,r c= X ) )
assume A6:
n in X
;
:: thesis: ex r being Real st
( r > 0 & Ball n,r c= X )
reconsider m =
n as
Point of
M by A1;
consider r being
Real such that A7:
r > 0
and A8:
Ball m,
r c= X
by A5, A6, PCOMPS_1:def 5;
consider r1 being
Real such that A9:
(
r1 > 0 &
Ball n,
r1 c= Ball m,
r )
by A2, A7;
take
r1
;
:: thesis: ( r1 > 0 & Ball n,r1 c= X )
thus
(
r1 > 0 &
Ball n,
r1 c= X )
by A8, A9, XBOOLE_1:1;
:: thesis: verum
end;
hence
X in Family_open_set N
by A1, A5, PCOMPS_1:def 5;
:: thesis: verum
end;
let X be
set ;
:: according to TARSKI:def 3 :: thesis: ( not X in Family_open_set N or X in Family_open_set M )
assume A10:
X in Family_open_set N
;
:: thesis: X in Family_open_set M
for
m being
Point of
M st
m in X holds
ex
r being
Real st
(
r > 0 &
Ball m,
r c= X )
proof
let m be
Point of
M;
:: thesis: ( m in X implies ex r being Real st
( r > 0 & Ball m,r c= X ) )
assume A11:
m in X
;
:: thesis: ex r being Real st
( r > 0 & Ball m,r c= X )
reconsider n =
m as
Point of
N by A1;
consider r being
Real such that A12:
r > 0
and A13:
Ball n,
r c= X
by A10, A11, PCOMPS_1:def 5;
consider r1 being
Real such that A14:
(
r1 > 0 &
Ball m,
r1 c= Ball n,
r )
by A3, A12;
take
r1
;
:: thesis: ( r1 > 0 & Ball m,r1 c= X )
thus
(
r1 > 0 &
Ball m,
r1 c= X )
by A13, A14, XBOOLE_1:1;
:: thesis: verum
end;
hence
X in Family_open_set M
by A1, A10, PCOMPS_1:def 5;
:: thesis: verum
end;
hence
TopSpaceMetr M = TopSpaceMetr N
by A1, A4; :: thesis: verum