:: by Marco Riccardi

::

:: Received June 6, 2011

:: Copyright (c) 2011-2019 Association of Mizar Users

registration

correctness

coherence

{} is {} -valued ;

by FUNCTOR0:1;

correctness

coherence

{} is onto ;

end;
coherence

{} is {} -valued ;

by FUNCTOR0:1;

correctness

coherence

{} is onto ;

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

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(b_{1},b_{2}) holds

R93(b_{2},b_{1})

end;
:: original: are_homeomorphic

redefine pred S,T are_homeomorphic ;

symmetry

for S, T being TopStruct st R93(b

R93(b

proof 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

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

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

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 )

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

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

T2 is second-countable

proof end;

::$CT

:: see MFOLD_0:10,11

:: 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

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) )

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))

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)|

|((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)

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 )

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

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

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

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 )

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

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 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 ) )

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);

ex b_{1} being Function of (TOP-REAL n),R^1 st

for q being Point of (TOP-REAL n) holds b_{1} . q = |(p,q)|

for b_{1}, b_{2} being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b_{1} . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds b_{2} . q = |(p,q)| ) holds

b_{1} = b_{2}

end;
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 for q being Point of (TOP-REAL n) holds it . q = |(p,q)|;

ex b

for q being Point of (TOP-REAL n) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines InnerProduct MFOLD_2:def 1 :

for n being Nat

for p being Point of (TOP-REAL n)

for b_{3} being Function of (TOP-REAL n),R^1 holds

( b_{3} = InnerProduct p iff for q being Point of (TOP-REAL n) holds b_{3} . q = |(p,q)| );

for n being Nat

for p being Point of (TOP-REAL n)

for b

( b

registration

let n be Nat;

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

correctness

coherence

InnerProduct p is continuous ;

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

correctness

coherence

InnerProduct p is continuous ;

proof end;

definition

let n be Nat;

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

coherence

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

end;
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 { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;

coherence

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

proof 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 } ;

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))

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))) )

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))) )

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);

coherence

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

end;
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 (TOP-REAL n) | (Plane (p,q));

coherence

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

proof 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));

for n being Nat

for p, q being Point of (TOP-REAL n) holds TPlane (p,q) = (TOP-REAL n) | (Plane (p,q));

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

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

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;

:: deftheorem defines TUnitSphere MFOLD_2:def 4 :

for n being Nat holds TUnitSphere n = Tunit_circle (n + 1);

for n being Nat holds TUnitSphere n = Tunit_circle (n + 1);

:: 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) ;

ex b_{1} 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_{1} . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

for b_{1}, b_{2} 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_{1} . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds

b_{2} . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) holds

b_{1} = b_{2}

end;
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 for q being Point of (TOP-REAL n) st q in S holds

it . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));

ex b

for q being Point of (TOP-REAL n) st q in S holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{4} being Function of S,(TPlane (p,(0. (TOP-REAL n)))) holds

( b_{4} = stereographic_projection (S,p) iff for q being Point of (TOP-REAL n) st q in S holds

b_{4} . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) );

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

( b

b

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

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;

correctness

coherence

TUnitSphere n is second-countable ;

coherence

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

coherence

TUnitSphere n is n -manifold ;

;

end;
correctness

coherence

TUnitSphere n is second-countable ;

proof end;

correctness coherence

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

proof end;

correctness coherence

TUnitSphere n is n -manifold ;

;