let n be Nat; for A, B being Subset of (TOP-REAL n) st A is closed & B is closed holds
for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
( h .: (Int A) = Int B & h .: (Fr A) = Fr B )
let A, B be Subset of (TOP-REAL n); ( A is closed & B is closed implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )
assume that
A1:
A is closed
and
A2:
B is closed
; for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
( h .: (Int A) = Int B & h .: (Fr A) = Fr B )
set TR = TOP-REAL n;
A3:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
A4:
Int B c= B
by TOPS_1:16;
A5:
[#] ((TOP-REAL n) | B) = B
by PRE_TOPC:def 5;
let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); ( h is being_homeomorphism implies ( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )
assume A6:
h is being_homeomorphism
; ( h .: (Int A) = Int B & h .: (Fr A) = Fr B )
A7:
dom h = [#] ((TOP-REAL n) | A)
by A6, TOPS_2:def 5;
A8:
rng h = [#] ((TOP-REAL n) | B)
by A6, TOPS_2:def 5;
A9: (Fr A) \/ (Int A) =
(A \ (Int A)) \/ (Int A)
by A1, TOPS_1:43
.=
A \/ (Int A)
by XBOOLE_1:39
.=
A
by TOPS_1:16, XBOOLE_1:12
;
thus A10:
h .: (Int A) = Int B
h .: (Fr A) = Fr Bproof
thus
h .: (Int A) c= Int B
XBOOLE_0:def 10 Int B c= h .: (Int A)
let y be
object ;
TARSKI:def 3 ( not y in Int B or y in h .: (Int A) )
assume A11:
y in Int B
;
y in h .: (Int A)
then consider x being
object such that A12:
x in dom h
and A13:
h . x = y
by A4, A8, A5, FUNCT_1:def 3;
reconsider x =
x as
Point of
(TOP-REAL n) by A7, A3, A12;
assume A14:
not
y in h .: (Int A)
;
contradiction
not
x in Int A
by A12, FUNCT_1:def 6, A14, A13;
then
x in Fr A
by A12, A9, A3, XBOOLE_0:def 3;
then
h . x in Fr B
by Th10, A1, A6;
hence
contradiction
by A11, A13, TOPS_1:39, XBOOLE_0:3;
verum
end;
Fr A = A \ (Int A)
by A1, TOPS_1:43;
then h .: (Fr A) =
(h .: A) \ (h .: (Int A))
by A6, FUNCT_1:64
.=
B \ (h .: (Int A))
by RELAT_1:113, A7, A8, A3, A5
.=
Fr B
by A10, A2, TOPS_1:43
;
hence
h .: (Fr A) = Fr B
; verum