let n, m be Nat; for T being non empty TopSpace
for A, B being Subset of T
for r, s being Real st r > 0 & s > 0 holds
for pA being Point of (TOP-REAL n)
for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m
let T be non empty TopSpace; for A, B being Subset of T
for r, s being Real st r > 0 & s > 0 holds
for pA being Point of (TOP-REAL n)
for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m
let A, B be Subset of T; for r, s being Real st r > 0 & s > 0 holds
for pA being Point of (TOP-REAL n)
for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m
let r, s be Real; ( r > 0 & s > 0 implies for pA being Point of (TOP-REAL n)
for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m )
assume that
A1:
r > 0
and
A2:
s > 0
; for pA being Point of (TOP-REAL n)
for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m
A3:
Int B c= B
by TOPS_1:16;
A4:
(Int A) /\ (Int B) c= Int B
by XBOOLE_1:17;
A5:
[#] (T | B) = B
by PRE_TOPC:def 5;
then reconsider IB = (Int A) /\ (Int B) as Subset of (T | B) by A3, A4, XBOOLE_1:1;
let pA be Point of (TOP-REAL n); for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m
let pB be Point of (TOP-REAL m); ( T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B implies n = m )
assume that
A6:
T | A, Tdisk (pA,r) are_homeomorphic
and
A7:
T | B, Tdisk (pB,s) are_homeomorphic
and
A8:
Int A meets Int B
; n = m
consider hB being Function of (T | B),(Tdisk (pB,s)) such that
A9:
hB is being_homeomorphism
by A7, T_0TOPSP:def 1;
A10:
(T | B) | IB = T | ((Int A) /\ (Int B))
by A3, A4, XBOOLE_1:1, PRE_TOPC:7;
A11:
[#] (Tdisk (pB,s)) = cl_Ball (pB,s)
by PRE_TOPC:def 5;
then reconsider hBI = hB .: IB as Subset of (TOP-REAL m) by XBOOLE_1:1;
A12:
(Int A) /\ (Int B) in the topology of T
by PRE_TOPC:def 2;
not (Int A) /\ (Int B) is empty
by A8;
then consider p being set such that
A13:
p in (Int A) /\ (Int B)
;
reconsider p = p as Point of T by A13;
A14:
dom hB = [#] (T | B)
by A9, TOPS_2:def 5;
then A15:
hB . p in hB .: IB
by A13, FUNCT_1:def 6;
p in Int B
by A13, XBOOLE_0:def 4;
then
not Tdisk (pB,s) is empty
by A14, A3;
then reconsider f = hB | IB as Function of ((T | B) | IB),((Tdisk (pB,s)) | (hB .: IB)) by A13, JORDAN24:12;
A16:
Int A c= A
by TOPS_1:16;
IB /\ B = IB
by A3, A4, XBOOLE_1:1, XBOOLE_1:28;
then
IB in the topology of (T | B)
by A12, A5, PRE_TOPC:def 4;
then
IB is open
by PRE_TOPC:def 2;
then
hB .: IB is open
by A13, A9, TOPGRP_1:25, A2;
then
not Int hBI is empty
by A13, A2, Th13;
then
not hBI is boundary
;
then A17:
ind hBI = m
by Th6;
A18:
(Int A) /\ (Int B) c= Int A
by XBOOLE_1:17;
A19:
(Tdisk (pB,s)) | (hB .: IB) = (TOP-REAL m) | hBI
by PRE_TOPC:7, A11;
then reconsider F = f as Function of (T | ((Int A) /\ (Int B))),((TOP-REAL m) | hBI) by A10;
F is being_homeomorphism
by A9, METRIZTS:2, A19, A10;
then A20:
F " is being_homeomorphism
by TOPS_2:56, A15;
consider hA being Function of (T | A),(Tdisk (pA,r)) such that
A21:
hA is being_homeomorphism
by A6, T_0TOPSP:def 1;
A22:
[#] (T | A) = A
by PRE_TOPC:def 5;
then reconsider IA = (Int A) /\ (Int B) as Subset of (T | A) by A16, A18, XBOOLE_1:1;
A23:
(T | A) | IA = T | ((Int A) /\ (Int B))
by A16, A18, XBOOLE_1:1, PRE_TOPC:7;
A24:
dom hA = [#] (T | A)
by A21, TOPS_2:def 5;
then A25:
hA . p in hA .: IA
by A13, FUNCT_1:def 6;
p in Int A
by A13, XBOOLE_0:def 4;
then
not Tdisk (pA,r) is empty
by A24, A16;
then reconsider g = hA | IA as Function of ((T | A) | IA),((Tdisk (pA,r)) | (hA .: IA)) by A13, JORDAN24:12;
A26:
[#] (Tdisk (pA,r)) = cl_Ball (pA,r)
by PRE_TOPC:def 5;
then reconsider hAI = hA .: IA as Subset of (TOP-REAL n) by XBOOLE_1:1;
A27:
(Tdisk (pA,r)) | (hA .: IA) = (TOP-REAL n) | hAI
by PRE_TOPC:7, A26;
then reconsider G = g as Function of (T | ((Int A) /\ (Int B))),((TOP-REAL n) | hAI) by A23;
reconsider GF = G * (F ") as Function of ((TOP-REAL m) | hBI),((TOP-REAL n) | hAI) by A13;
G is being_homeomorphism
by A21, METRIZTS:2, A27, A23;
then
GF is being_homeomorphism
by A20, TOPS_2:57, A25, A15, A13;
then
hBI,hAI are_homeomorphic
by T_0TOPSP:def 1, METRIZTS:def 1;
then A28:
ind hBI = ind hAI
by TOPDIM_1:27;
IA /\ A = IA
by A16, A18, XBOOLE_1:1, XBOOLE_1:28;
then
IA in the topology of (T | A)
by A12, A22, PRE_TOPC:def 4;
then
IA is open
by PRE_TOPC:def 2;
then
hA .: IA is open
by A13, A21, TOPGRP_1:25, A1;
then
not Int hAI is empty
by A13, A1, Th13;
then
not hAI is boundary
;
hence
n = m
by A17, Th6, A28; verum