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


begin

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 R91(b1,b2) holds
R91(b2,b1)
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 Th5: :: 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 Th8: :: 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 Th11: :: MFOLD_2:11
for n being Nat
for M, N being non empty TopSpace st M is n -locally_euclidean & M,N are_homeomorphic holds
N is n -locally_euclidean
proof end;

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 k, n 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 number 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 b1 being Function of (TOP-REAL n),R^1 st
for q being Point of (TOP-REAL n) holds b1 . q = |(p,q)|
proof end;
uniqueness
for b1, b2 being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b1 . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds b2 . q = |(p,q)| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines InnerProduct MFOLD_2:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for b3 being Function of (TOP-REAL n),R^1 holds
( b3 = InnerProduct p iff for q being Point of (TOP-REAL n) holds b3 . 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;

begin

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 p1, p, 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;

begin

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 b1 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st
for q being Point of (TOP-REAL n) st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
proof end;
uniqueness
for b1, b2 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st ( for q being Point of (TOP-REAL n) st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds
b2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) holds
b1 = b2
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 b4 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) holds
( b4 = stereographic_projection (S,p) iff for q being Point of (TOP-REAL n) st q in S holds
b4 . 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 ;
proof end;
cluster TUnitSphere n -> n -locally_euclidean ;
correctness
coherence
TUnitSphere n is n -locally_euclidean ;
proof end;
cluster TUnitSphere n -> n -manifold ;
correctness
coherence
TUnitSphere n is n -manifold ;
;
end;