set M = TUnitSphere n;
for p being Point of (TUnitSphere n) ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
proof
let p be
Point of
(TUnitSphere n);
ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
reconsider n1 =
n + 1 as
Element of
NAT by ORDINAL1:def 12;
[#] (Tunit_circle (n + 1)) c= [#] (TOP-REAL (n + 1))
by PRE_TOPC:def 4;
then reconsider p1 =
p as
Point of
(TOP-REAL n1) ;
A1:
|.p1.| = 1
by TOPREALB:12;
A2:
|.(- p1).| =
sqrt |((- p1),(- p1))|
by EUCLID_2:37
.=
sqrt |(p1,p1)|
by EUCLID_2:23
.=
1
by A1, EUCLID_2:37
;
then
|.((- p1) + (0. (TOP-REAL n1))).| = 1
by RLVECT_1:4;
then
|.((- p1) + ((- 1) * (0. (TOP-REAL n1)))).| = 1
by RLVECT_1:10;
then B3:
|.((- p1) - (0. (TOP-REAL n1))).| = 1
by RLVECT_1:16;
then
- p1 in Sphere (
(0. (TOP-REAL n1)),1)
by TOPREAL9:9;
then
- p1 in [#] ((TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1)))
by PRE_TOPC:def 5;
then
- p1 in the
carrier of
(Tcircle ((0. (TOP-REAL n1)),1))
by TOPREALB:def 6;
then
- p1 in the
carrier of
(Tunit_circle n1)
by TOPREALB:def 7;
then reconsider A =
{(- p1)} as
Subset of
(TUnitSphere n) by ZFMISC_1:31;
reconsider U1 =
([#] (TUnitSphere n)) \ A as
Subset of
(TUnitSphere n) ;
|.(0. (TOP-REAL n1)).| <> |.(- p1).|
by A2, EUCLID_2:39;
then
0. (TOP-REAL n1) <> (1 + 1) * (- p1)
by RLVECT_1:11;
then
0. (TOP-REAL n1) <> (1 * (- p1)) + (1 * (- p1))
by RLVECT_1:def 6;
then
0. (TOP-REAL n1) <> (1 * (- p1)) + (- p1)
by RLVECT_1:def 8;
then
0. (TOP-REAL n1) <> (- p1) + (- p1)
by RLVECT_1:def 8;
then
(- p1) + (- (- p1)) <> (- p1) + (- p1)
by RLVECT_1:5;
then A4:
not
p1 in {(- p1)}
by TARSKI:def 1;
then
p1 in U1
by XBOOLE_0:def 5;
then reconsider U =
U1 as
a_neighborhood of
p by CONNSP_2:3, FRECHET:4;
take
U
;
U, [#] (TOP-REAL n) are_homeomorphic
reconsider m =
n + 1 as
Nat ;
A5:
TUnitSphere n =
Tcircle (
(0. (TOP-REAL m)),1)
by TOPREALB:def 7
.=
(TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1))
by TOPREALB:def 6
;
reconsider S =
Sphere (
(0. (TOP-REAL m)),1) as
Subset of
(TOP-REAL m) ;
reconsider U11 =
U1 as
Subset of
((TOP-REAL m) | S) by A5;
U1 c= [#] (Tunit_circle m)
;
then A6:
U1 c= Sphere (
(0. (TOP-REAL m)),1)
by A5, PRE_TOPC:def 5;
then reconsider V =
U11 as non
empty Subset of
(TOP-REAL m) by A4, XBOOLE_0:def 5, XBOOLE_1:1;
(TUnitSphere n) | U = (TOP-REAL m) | V
by A5, A6, PRE_TOPC:7;
then reconsider U2 =
(TUnitSphere n) | U as non
empty SubSpace of
TOP-REAL m ;
reconsider p2 =
- p1 as
Point of
(TOP-REAL m) ;
p2 <> 0. (TOP-REAL m)
by A2, EUCLID_2:39;
then A7:
TOP-REAL n,
TPlane (
p2,
(0. (TOP-REAL m)))
are_homeomorphic
by Th29;
A8:
(TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
by TSEP_1:93;
A9:
TOP-REAL n,
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
are_homeomorphic
by YELLOW14:19;
[#] U2 =
U
by PRE_TOPC:def 5
.=
the
carrier of
(Tcircle ((0. (TOP-REAL m)),1)) \ {p2}
by TOPREALB:def 7
.=
([#] ((TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)))) \ {p2}
by TOPREALB:def 6
.=
(Sphere ((0. (TOP-REAL m)),1)) \ {p2}
by PRE_TOPC:def 5
;
then
stereographic_projection (
U2,
p2) is
being_homeomorphism
by B3, TOPREAL9:9, Th31;
then
U2,
TPlane (
p2,
(0. (TOP-REAL m)))
are_homeomorphic
by T_0TOPSP:def 1;
then
TOP-REAL n,
U2 are_homeomorphic
by A7, BORSUK_3:3;
hence
U,
[#] (TOP-REAL n) are_homeomorphic
by A8, METRIZTS:def 1, A9, BORSUK_3:3;
verum
end;
hence
( TUnitSphere n is without_boundary & TUnitSphere n is n -locally_euclidean )
by MFOLD_1:14; verum