let n be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( h is being_homeomorphism implies ( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )
assume A6: h is being_homeomorphism ; :: thesis: ( 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 :: thesis: h .: (Fr A) = Fr B
proof
thus h .: (Int A) c= Int B :: according to XBOOLE_0:def 10 :: thesis: Int B c= h .: (Int A)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in h .: (Int A) or y in Int B )
assume y in h .: (Int A) ; :: thesis: y in Int B
then ex x being object st
( x in dom h & x in Int A & h . x = y ) by FUNCT_1:def 6;
hence y in Int B by A2, A6, Th11; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Int B or y in h .: (Int A) )
assume A11: y in Int B ; :: thesis: 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) ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum