let M, N be non empty TopSpace; for p being Point of M
for U being a_neighborhood of p
for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
let p be Point of M; for U being a_neighborhood of p
for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
let U be a_neighborhood of p; for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
let B be open Subset of N; ( U,B are_homeomorphic implies ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic ) )
assume A0:
U,B are_homeomorphic
; ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
then A1:
M | U,N | B are_homeomorphic
by METRIZTS:def 1;
consider f being Function of (M | U),(N | B) such that
A2:
f is being_homeomorphism
by T_0TOPSP:def 1, A0, METRIZTS:def 1;
consider V being Subset of M such that
A3:
( V is open & V c= U & p in V )
by CONNSP_2:6;
V c= [#] (M | U)
by A3, PRE_TOPC:def 5;
then reconsider V1 = V as Subset of (M | U) ;
reconsider M1 = M | U as non empty TopStruct by A3;
reconsider N1 = N | B as non empty TopStruct by A3, A1, YELLOW14:18;
reconsider f1 = f as Function of M1,N1 ;
rng f c= [#] (N | B)
;
then A4:
rng f c= B
by PRE_TOPC:def 5;
A5:
(M | U) | V1,(N | B) | (f .: V1) are_homeomorphic
by METRIZTS:def 1, A2, METRIZTS:3;
reconsider V = V as open Subset of M by A3;
B = the carrier of (N | B)
by PRE_TOPC:8;
then reconsider N1 = N | B as open SubSpace of N by TSEP_1:16;
B c= the carrier of N
;
then
[#] (N | B) c= the carrier of N
by PRE_TOPC:def 5;
then reconsider S = f .: V1 as Subset of N by XBOOLE_1:1;
reconsider S1 = f .: V1 as Subset of N1 ;
A6:
for P being Subset of M1 holds
( P is open iff f1 .: P is open )
by A2, TOPGRP_1:25;
A7:
V in the topology of M
by PRE_TOPC:def 2;
V1 = V /\ ([#] M1)
by XBOOLE_1:28;
then
V1 in the topology of M1
by A7, PRE_TOPC:def 4;
then
S1 is open
by A6, PRE_TOPC:def 2;
then reconsider S = S as open Subset of N by TSEP_1:17;
take
V
; ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
take
S
; ( V c= U & p in V & V,S are_homeomorphic )
thus
( V c= U & p in V )
by A3; V,S are_homeomorphic
A8:
(M | U) | V1 = M | V
by A3, PRE_TOPC:7;
f .: U c= rng f
by RELAT_1:111;
then A9:
f .: U c= B
by A4;
f .: V c= f .: U
by A3, RELAT_1:123;
then
(N | B) | (f .: V1) = N | S
by A9, PRE_TOPC:7, XBOOLE_1:1;
hence
V,S are_homeomorphic
by A5, A8, METRIZTS:def 1; verum