let n be Nat; :: thesis: for M being non empty TopSpace
for q being Point of M
for r being real number
for p being Point of (TOP-REAL n) st r > 0 holds
for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
let M be non empty TopSpace; :: thesis: for q being Point of M
for r being real number
for p being Point of (TOP-REAL n) st r > 0 holds
for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
set TR = TOP-REAL n;
let q be Point of M; :: thesis: for r being real number
for p being Point of (TOP-REAL n) st r > 0 holds
for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
let r be real number ; :: thesis: for p being Point of (TOP-REAL n) st r > 0 holds
for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
let p be Point of (TOP-REAL n); :: thesis: ( r > 0 implies for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic ) )
assume A1: r > 0 ; :: thesis: for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
let U be a_neighborhood of q; :: thesis: ( M | U, Tball (p,r) are_homeomorphic implies ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic ) )
assume A2: M | U, Tball (p,r) are_homeomorphic ; :: thesis: ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )
A3: [#] (M | U) = U by PRE_TOPC:def 5;
then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;
set MU = M | U;
consider h being Function of (M | U),(Tball (p,r)) such that
A4: h is being_homeomorphism by T_0TOPSP:def 1, A2;
A5: dom h = [#] (M | U) by A4, TOPS_2:def 5;
A7: [#] (Tball (p,r)) = Ball (p,r) by PRE_TOPC:def 5;
then reconsider W = h .: IU as Subset of (TOP-REAL n) by XBOOLE_1:1;
IU is open by TSEP_1:9;
then h .: IU is open by A4, TOPGRP_1:25, A1;
then reconsider W = W as open Subset of (TOP-REAL n) by A7, TSEP_1:9;
q in Int U by CONNSP_2:def 1;
then A8: h . q in W by A5, FUNCT_1:def 6;
then reconsider hq = h . q as Point of (TOP-REAL n) ;
reconsider HQ = hq as Point of (Euclid n) by EUCLID:67;
Int W = W by TOPS_1:23;
then consider s being Real such that
A9: s > 0 and
A10: Ball (HQ,s) c= W by A8, GOBOARD6:5;
set m = s / 2;
A11: Ball (HQ,s) = Ball (hq,s) by TOPREAL9:13;
set CL = cl_Ball (hq,(s / 2));
A12: n in NAT by ORDINAL1:def 12;
A13: cl_Ball (hq,(s / 2)) c= Ball (hq,s) by A9, A12, XREAL_1:216, JORDAN:21;
then cl_Ball (hq,(s / 2)) c= W by A10, A11;
then A14: cl_Ball (hq,(s / 2)) c= Ball (p,r) by A7, XBOOLE_1:1;
set BB = Ball (hq,(s / 2));
A15: Ball (hq,(s / 2)) c= cl_Ball (hq,(s / 2)) by TOPREAL9:16;
then reconsider CL = cl_Ball (hq,(s / 2)), BB = Ball (hq,(s / 2)) as Subset of (Tball (p,r)) by A14, XBOOLE_1:1, A7;
A16: rng h = [#] (Tball (p,r)) by A4, TOPS_2:def 5;
A17: q in Int U by CONNSP_2:def 1;
A18: Int U c= U by TOPS_1:16;
reconsider hBB = h " BB as Subset of M by A3, XBOOLE_1:1;
hq is Element of REAL n by EUCLID:22;
then |.(hq - hq).| = 0 ;
then hq in BB by A9;
then A19: q in hBB by FUNCT_1:def 7, A5, A18, A17, A3;
A20: dom h = [#] (M | U) by A4, TOPS_2:def 5;
A21: h " W = IU by FUNCT_1:82, A4, FUNCT_1:76, A20;
CL meets Ball (p,r) by A9, A7, XBOOLE_1:67;
then reconsider hCL = h " CL as non empty Subset of (M | U) by A7, RELAT_1:138, A16;
A22: h .: hCL = CL by FUNCT_1:77, A16;
A23: (Tball (p,r)) | CL = (TOP-REAL n) | (cl_Ball (hq,(s / 2))) by A7, PRE_TOPC:7;
then reconsider HH = h | hCL as Function of ((M | U) | hCL),(Tdisk (hq,(s / 2))) by A22, A1, JORDAN24:12;
HH is being_homeomorphism by A22, A23, A4, METRIZTS:2;
then A24: (M | U) | hCL, Tdisk (hq,(s / 2)) are_homeomorphic by T_0TOPSP:def 1;
Tdisk (hq,(s / 2)), Tdisk (p,r) are_homeomorphic by A1, A9, Lm1;
then A25: (M | U) | hCL, Tdisk (p,r) are_homeomorphic by A1, A9, BORSUK_3:3, A24;
reconsider HCL = hCL as Subset of M by A3, XBOOLE_1:1;
A26: (M | U) | hCL = M | HCL by PRE_TOPC:7, A3;
BB c= W by A10, A11, A13, A15;
then A27: h " BB c= h " W by RELAT_1:143;
BB is open by TSEP_1:9;
then h " BB is open by A4, TOPGRP_1:26, A1;
then hBB is open by A21, A27, TSEP_1:9;
then q in Int HCL by RELAT_1:143, A15, A19, TOPS_1:22;
then A28: HCL is a_neighborhood of q by CONNSP_2:def 1;
CL c= W by A13, A10, A11;
hence ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic ) by A28, RELAT_1:143, A21, A25, A26; :: thesis: verum