let n be natural number ; for M, N being non empty TopSpace st M is n -locally_euclidean & M,N are_homeomorphic holds
N is n -locally_euclidean
let M, N be non empty TopSpace; ( M is n -locally_euclidean & M,N are_homeomorphic implies N is n -locally_euclidean )
assume A1:
M is n -locally_euclidean
; ( not M,N are_homeomorphic or N is n -locally_euclidean )
assume
M,N are_homeomorphic
; N is n -locally_euclidean
then consider f being Function of N,M such that
A2:
f is being_homeomorphism
by T_0TOPSP:def 1;
A3:
( dom f = [#] N & rng f = [#] M & f is one-to-one & f is continuous & f " is continuous )
by A2, TOPS_2:def 5;
for q being Point of N ex U being a_neighborhood of q ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
proof
let q be
Point of
N;
ex U being a_neighborhood of q ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
set p =
f . q;
consider U1 being
a_neighborhood of
f . q,
S1 being
open Subset of
(TOP-REAL n) such that A4:
U1,
S1 are_homeomorphic
by A1, MFOLD_1:def 4;
consider U2 being
open Subset of
M,
S being
open Subset of
(TOP-REAL n) such that A5:
(
U2 c= U1 &
f . q in U2 &
U2,
S are_homeomorphic )
by A4, MFOLD_1:11;
A6:
f " U2 is
open
by A3, TOPS_2:43;
q in f " U2
by A5, FUNCT_2:38;
then reconsider U =
f " U2 as
a_neighborhood of
q by A6, CONNSP_2:6;
take
U
;
ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take
S
;
U,S are_homeomorphic
U,
U2 are_homeomorphic
by A2, Th5;
hence
U,
S are_homeomorphic
by A5, Th8;
verum
end;
hence
N is n -locally_euclidean
by MFOLD_1:def 4; verum