:: Planes and Spheres as Topological Manifolds. Stereographic Projection
:: by Marco Riccardi
::
:: Received June 6, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users

registration

cluster {} -> {} -valued ;

correctness
coherence
{} is {} -valued ;
by FUNCTOR0:1;

cluster {} -> onto ;

correctness
coherence
{} is onto ;

proof end;

end;

theorem Th1: :: MFOLD_2:1

for f being Function
for Y being set holds dom (Y |` f) = f " Y

proof end;

theorem Th2: :: MFOLD_2:2

for f being Function
for Y1, Y2 being set st Y2 c= Y1 holds
(Y1 |` f) " Y2 = f " Y2

proof end;

:: generalization TOPS_2 Th70

theorem Th3: :: MFOLD_2:3

for S, T being TopStruct
for f being Function of S,T st f is being_homeomorphism holds
f " is being_homeomorphism

proof end;

definition

let S, T be TopStruct ;
:: original: are_homeomorphic
redefine pred S,T are_homeomorphic ;
symmetry
for S, T being TopStruct st R94(b₁,b₂) holds
R94(b₂,b₁)

proof end;

end;

:: like METRIZTS

theorem Th4: :: MFOLD_2:4

for T1, T2 being TopSpace
for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism

proof end;

theorem :: MFOLD_2:5

for T1, T2 being TopSpace
for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
f " A2,A2 are_homeomorphic

proof end;

theorem :: MFOLD_2:6

for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
A2,A1 are_homeomorphic

proof end;

theorem Th7: :: MFOLD_2:7

for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is empty iff A2 is empty )

proof end;

theorem :: MFOLD_2:8

for T1, T2, T3 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2
for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic

proof end;

theorem Th9: :: MFOLD_2:9

for T1, T2 being TopSpace st T1 is second-countable & T1,T2 are_homeomorphic holds
T2 is second-countable

proof end;

theorem Th10: :: MFOLD_2:10

for M, N being non empty TopSpace st M is Hausdorff & M,N are_homeomorphic holds
N is Hausdorff

proof end;

theorem :: MFOLD_2:11

canceled;

::$CT
:: see MFOLD_0:10,11

theorem Th12: :: MFOLD_2:12

for n being Nat
for M, N being non empty TopSpace st M is n -manifold & M,N are_homeomorphic holds
N is n -manifold

proof end;

:: like MATRIX14

theorem Th13: :: MFOLD_2:13

for x1, x2 being FinSequence of REAL
for i being Element of NAT st i in dom (mlt (x1,x2)) holds
( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )

proof end;

theorem Th14: :: MFOLD_2:14

for x1, x2, y1, y2 being FinSequence of REAL st len x1 = len x2 & len y1 = len y2 holds
mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))

proof end;

theorem Th15: :: MFOLD_2:15

for x1, x2, y1, y2 being FinSequence of REAL st len x1 = len x2 & len y1 = len y2 holds
|((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|

proof end;

Lm1: for n being Nat holds the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n)

proof end;

Lm2: for n being Nat holds 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n)

proof end;

theorem Th16: :: MFOLD_2:16

for n, k being Nat
for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds
(p1 + p2) . k = (p1 . k) + (p2 . k)

proof end;

:: like MATRTOP_2

theorem Th17: :: MFOLD_2:17

for n being Nat
for X being set holds
( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n )

proof end;

theorem Th18: :: MFOLD_2:18

for n being Nat
for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (RealVectSpace (Seg n))
for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv

proof end;

theorem Th19: :: MFOLD_2:19

for n being Nat
for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv

proof end;

theorem Th20: :: MFOLD_2:20

for n being Nat
for Lv being Linear_Combination of RealVectSpace (Seg n)
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv

proof end;

theorem Th21: :: MFOLD_2:21

for n being Nat
for Af being Subset of (RealVectSpace (Seg n))
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )

proof end;

theorem Th22: :: MFOLD_2:22

for n being Nat
for p being Point of (TOP-REAL n)
for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l

proof end;

theorem :: MFOLD_2:23

for n being Nat holds RN_Base n is Basis of TOP-REAL n

proof end;

theorem Th24: :: MFOLD_2:24

for n being Nat
for V being Subset of (TOP-REAL n) holds
( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) )

proof end;

definition

let n be Nat;
let p be Point of (TOP-REAL n);

func InnerProduct p -> Function of (TOP-REAL n),R^1 means :Def1: :: MFOLD_2:def 1
for q being Point of (TOP-REAL n) holds it . q = |(p,q)|;

existence
ex b₁ being Function of (TOP-REAL n),R^1 st
for q being Point of (TOP-REAL n) holds b₁ . q = |(p,q)|

proof end;

uniqueness
for b₁, b₂ being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b₁ . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds b₂ . q = |(p,q)| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines InnerProduct MFOLD_2:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for b₃ being Function of (TOP-REAL n),R^1 holds
( b₃ = InnerProduct p iff for q being Point of (TOP-REAL n) holds b₃ . q = |(p,q)| );

registration

let n be Nat;
let p be Point of (TOP-REAL n);

cluster InnerProduct p -> continuous ;

correctness
coherence
InnerProduct p is continuous ;

proof end;

end;

definition

let n be Nat;
let p, q be Point of (TOP-REAL n);

func Plane (p,q) -> Subset of (TOP-REAL n) equals :: MFOLD_2:def 2
{ y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;

correctness
coherence
{ y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } is Subset of (TOP-REAL n);

proof end;

end;

:: deftheorem defines Plane MFOLD_2:def 2 :
for n being Nat
for p, q being Point of (TOP-REAL n) holds Plane (p,q) = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;

theorem Th25: :: MFOLD_2:25

for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) holds (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))

proof end;

theorem Th26: :: MFOLD_2:26

for n being Nat
for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )

proof end;

theorem Th27: :: MFOLD_2:27

for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) holds
ex R being Function of (TOP-REAL n),(TOP-REAL n) st
( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) )

proof end;

definition

let n be Nat;
let p, q be Point of (TOP-REAL n);

func TPlane (p,q) -> non empty SubSpace of TOP-REAL n equals :: MFOLD_2:def 3
(TOP-REAL n) | (Plane (p,q));

correctness
coherence
(TOP-REAL n) | (Plane (p,q)) is non empty SubSpace of TOP-REAL n;

proof end;

end;

:: deftheorem defines TPlane MFOLD_2:def 3 :
for n being Nat
for p, q being Point of (TOP-REAL n) holds TPlane (p,q) = (TOP-REAL n) | (Plane (p,q));

theorem Th28: :: MFOLD_2:28

for n being Nat holds Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*>

proof end;

Lm3: for n being Nat
for p0 being Point of (TOP-REAL (n + 1)) st p0 = Base_FinSeq ((n + 1),(n + 1)) holds
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic

proof end;

theorem Th29: :: MFOLD_2:29

for n being Nat
for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TOP-REAL n, TPlane (p,q) are_homeomorphic

proof end;

theorem :: MFOLD_2:30

for n being Nat
for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TPlane (p,q) is n -manifold

proof end;

definition

let n be Nat;

func TUnitSphere n -> TopSpace equals :: MFOLD_2:def 4
Tunit_circle (n + 1);

correctness
coherence
Tunit_circle (n + 1) is TopSpace;
;

end;

:: deftheorem defines TUnitSphere MFOLD_2:def 4 :
for n being Nat holds TUnitSphere n = Tunit_circle (n + 1);

registration

let n be Nat;

cluster TUnitSphere n -> non empty ;

correctness
coherence
not TUnitSphere n is empty ;
;

end;

:: stereographic projection

definition

let n be Nat;
let p be Point of (TOP-REAL n);
let S be SubSpace of TOP-REAL n;
assume A1: p in Sphere ((0. (TOP-REAL n)),1) ;

func stereographic_projection (S,p) -> Function of S,(TPlane (p,(0. (TOP-REAL n)))) means :Def5: :: MFOLD_2:def 5
for q being Point of (TOP-REAL n) st q in S holds
it . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));

existence
ex b₁ being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st
for q being Point of (TOP-REAL n) st q in S holds
b₁ . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

proof end;

uniqueness
for b₁, b₂ being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st ( for q being Point of (TOP-REAL n) st q in S holds
b₁ . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds
b₂ . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines stereographic_projection MFOLD_2:def 5 :
for n being Nat
for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st p in Sphere ((0. (TOP-REAL n)),1) holds
for b₄ being Function of S,(TPlane (p,(0. (TOP-REAL n)))) holds
( b₄ = stereographic_projection (S,p) iff for q being Point of (TOP-REAL n) st q in S holds
b₄ . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) );

theorem Th31: :: MFOLD_2:31

for n being Nat
for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds
stereographic_projection (S,p) is being_homeomorphism

proof end;

registration

let n be Nat;

cluster TUnitSphere n -> second-countable ;

correctness
coherence
TUnitSphere n is second-countable ;
;

cluster TUnitSphere n -> n -locally_euclidean without_boundary ;

correctness
coherence
( TUnitSphere n is without_boundary & TUnitSphere n is n -locally_euclidean );

proof end;

cluster TUnitSphere n -> n -manifold ;

correctness
coherence
TUnitSphere n is n -manifold ;
;

end;