begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
Lm1:
for n being natural number holds the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n)
Lm2:
for n being natural number holds 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n)
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
:: deftheorem Def2 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)| );
begin
:: deftheorem defines Plane MFOLD_2:def 2 :
for n being natural number
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:
theorem Th26:
theorem Th27:
:: deftheorem defines TPlane MFOLD_2:def 3 :
for n being natural number
for p, q being Point of (TOP-REAL n) holds TPlane (p,q) = (TOP-REAL n) | (Plane (p,q));
theorem Th28:
Lm3:
for n being natural number
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
theorem Th29:
theorem
begin
:: deftheorem defines TUnitSphere MFOLD_2:def 4 :
for n being natural number holds TUnitSphere n = Tunit_circle (n + 1);
definition
let n be
natural number ;
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 :
Def4:
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))
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
end;
:: deftheorem Def4 defines stereographic_projection MFOLD_2:def 5 :
for n being natural number
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: