:: Planes and Spheres as Topological Manifolds. Stereographic Projection
:: by Marco Riccardi
::
:: Copyright (c) 2011-2019 Association of Mizar Users

registration
correctness
coherence ;
by FUNCTOR0:1;
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 R93(b1,b2) holds
R93(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 :: 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 ()
proof end;

Lm2: for n being Nat holds 0. (RealVectSpace (Seg n)) = 0. ()
proof end;

theorem Th16: :: MFOLD_2:16
for n, k being Nat
for p1, p2 being Point of () 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 ()
for fr being Function of (),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 ()
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 () 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 ()
for V being Subset of () 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 () holds
( V in the topology of () iff for p being Point of () 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 ();
func InnerProduct p -> Function of (),R^1 means :Def1: :: MFOLD_2:def 1
for q being Point of () holds it . q = |(p,q)|;
existence
ex b1 being Function of (),R^1 st
for q being Point of () holds b1 . q = |(p,q)|
proof end;
uniqueness
for b1, b2 being Function of (),R^1 st ( for q being Point of () holds b1 . q = |(p,q)| ) & ( for q being Point of () 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 ()
for b3 being Function of (),R^1 holds
( b3 = InnerProduct p iff for q being Point of () holds b3 . q = |(p,q)| );

registration
let n be Nat;
let p be Point of ();
correctness
coherence ;
proof end;
end;

definition
let n be Nat;
let p, q be Point of ();
func Plane (p,q) -> Subset of () equals :: MFOLD_2:def 2
{ y where y is Point of () : |(p,(y - q))| = 0 } ;
correctness
coherence
{ y where y is Point of () : |(p,(y - q))| = 0 } is Subset of ()
;
proof end;
end;

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

theorem Th25: :: MFOLD_2:25
for n being Nat
for p, p1, p2 being Point of () holds (transl (p1,())) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
proof end;

theorem Th26: :: MFOLD_2:26
for n being Nat
for p being Point of () st p <> 0. () holds
ex A being linearly-independent Subset of () st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. ())) )
proof end;

theorem Th27: :: MFOLD_2:27
for n being Nat
for p1, p2 being Point of () st p1 <> 0. () & p2 <> 0. () holds
ex R being Function of (),() st
( R is being_homeomorphism & R .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) )
proof end;

definition
let n be Nat;
let p, q be Point of ();
func TPlane (p,q) -> non empty SubSpace of TOP-REAL n equals :: MFOLD_2:def 3
() | (Plane (p,q));
correctness
coherence
() | (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 () holds TPlane (p,q) = () | (Plane (p,q));

theorem Th28: :: MFOLD_2:28
for n being Nat holds Base_FinSeq ((n + 1),(n + 1)) = (0. ()) ^ <*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 ();
let S be SubSpace of TOP-REAL n;
assume A1: p in Sphere ((0. ()),1) ;
func stereographic_projection (S,p) -> Function of S,(TPlane (p,(0. ()))) means :Def5: :: MFOLD_2:def 5
for q being Point of () 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. ()))) st
for q being Point of () 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. ()))) st ( for q being Point of () st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of () 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 ()
for S being SubSpace of TOP-REAL n st p in Sphere ((0. ()),1) holds
for b4 being Function of S,(TPlane (p,(0. ()))) holds
( b4 = stereographic_projection (S,p) iff for q being Point of () 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 ()
for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. ()),1)) \ {p} & p in Sphere ((0. ()),1) holds
stereographic_projection (S,p) is being_homeomorphism
proof end;

registration
let n be Nat;
correctness
proof end;
correctness
coherence ;
proof end;
correctness
coherence ;
;
end;