:: Planes and Spheres as Topological Manifolds. Stereographic Projection
:: by Marco Riccardi
::
:: Received June 6, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, ORDINAL1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3,
SUPINF_2, XBOOLE_0, PRVECT_1, FUNCOP_1, XXREAL_0, RLSUB_2, ORDINAL2,
METRIC_1, TARSKI, STRUCT_0, REAL_1, MATRIXR2, FINSEQ_1, FINSEQ_2,
COMPTS_1, BINOP_2, TOPS_2, T_0TOPSP, CONNSP_2, FUNCT_1, RELAT_1, CARD_1,
FUNCT_2, VALUED_1, WAYBEL23, RLVECT_3, FINSET_1, NAT_1, PARTFUN1,
SETFAM_1, ORDINAL4, ALGSTR_0, EUCLID_7, CARD_3, RCOMP_1, TOPREALB,
RVSUM_1, RLSUB_1, RLVECT_2, FUNCSDOM, RLVECT_1, RLTOPSP1, VECTSP_1,
MATRIX_1, MATRLIN2, RLVECT_5, ZFMISC_1, PCOMPS_1, COMPLEX1, SQUARE_1,
TOPMETR, INCSP_1, MFOLD_0, MFOLD_1, MFOLD_2;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCOP_1, FUNCT_1, TOPS_2,
RELAT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, NUMBERS,
XREAL_0, XXREAL_0, COMPLEX1, REAL_1, NAT_1, RVSUM_1, PRE_TOPC, METRIC_1,
TOPREAL9, CONNSP_2, METRIZTS, COMPTS_1, EUCLID, SQUARE_1, TOPMETR,
TMAP_1, WAYBEL23, CARD_1, TOPREALB, RLSUB_1, RLVECT_3, RLTOPSP1,
PRVECT_1, VECTSP_1, MATRIX_1, MATRIX_6, MATRTOP1, RLVECT_2, RLVECT_5,
FUNCSDOM, FINSEQ_1, FINSET_1, FINSEQ_2, EUCLID_7, STRUCT_0, RLVECT_1,
RLSUB_2, T_0TOPSP, XCMPLX_0, BINOP_2, ZFMISC_1, NAT_D, PCOMPS_1, MFOLD_0,
MFOLD_1;
constructors MONOID_0, TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, METRIZTS,
PCOMPS_1, COMPTS_1, BINOP_2, TMAP_1, WAYBEL23, RLVECT_3, PRVECT_1,
MATRIX_6, MATRTOP1, RLVECT_5, EUCLID_7, FVSUM_1, RLSUB_2, BORSUK_3,
NAT_D, CONVEX1, MFOLD_0, MFOLD_1, REAL_1;
registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, SQUARE_1, NAT_1,
STRUCT_0, METRIC_1, MONOID_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1,
RELAT_1, PRE_TOPC, TOPS_1, TOPREAL9, TMAP_1, COMPTS_1, TOPMETR, RLVECT_3,
TOPREAL1, SUBSET_1, TOPREALB, VECTSP_1, EUCLID_7, FINSET_1, FUNCT_2,
FINSEQ_2, RLSUB_1, ORDINAL1, MATRTOP1, RVSUM_1, NUMBERS, RLTOPSP1,
RELSET_1, MFOLD_0, MFOLD_1, RLAFFIN3;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, FUNCT_1;
equalities EUCLID, FINSEQ_1, STRUCT_0, VECTSP_1, RLVECT_1;
expansions FINSEQ_1, STRUCT_0, TARSKI, FUNCT_1;
theorems TOPREAL9, TOPREALB, METRIZTS, TSEP_1, YELLOW14, T_0TOPSP, RLVECT_5,
ZFMISC_1, TARSKI, RELAT_1, FUNCT_1, RLTOPSP1, EUCLID, FUNCT_2, RLSUB_1,
XBOOLE_0, EUCLID_2, JGRAPH_5, ORDINAL1, RLVECT_3, MATRTOP2, FUNCSDOM,
FINSEQ_2, EUCLID_7, CARD_1, RLVECT_2, RLVECT_1, NAT_1, PARTFUN1,
FINSEQ_3, MATRIX13, FINSEQ_1, RLSUB_2, RLVECT_4, XCMPLX_1, PRE_TOPC,
WAYBEL23, TOPS_2, BORSUK_3, CONNSP_2, XBOOLE_1, TSP_1, SUBSET_1, RVSUM_1,
FUNCOP_1, VALUED_1, MATRIXR2, RELSET_1, XREAL_1, FINSEQ_4, PCOMPS_1,
XREAL_0, JORDAN, REAL_NS1, SQUARE_1, XXREAL_0, METRIC_1, TOPMETR,
TOPREAL3, UNIFORM1, JGRAPH_1, JGRAPH_2, JGRAPH_6, TMAP_1, JORDAN2C,
FRECHET, MFOLD_1, FUNCTOR0, RLAFFIN3, XTUPLE_0, MFOLD_0;
schemes NAT_1, FUNCT_2, CLASSES1;
begin :: Preliminaries
registration
cluster {} -> {}-valued;
correctness by FUNCTOR0:1;
cluster {} -> onto;
correctness
proof
rng {} = {};
hence thesis by FUNCT_2:def 3;
end;
end;
theorem Th1:
for f being Function, Y being set holds dom(Y|`f) = f"Y
proof
let f be Function;
let Y be set;
for x being object holds x in dom(Y|`f) iff x in f"Y
proof
let x be object;
hereby
assume x in dom(Y|`f);
then consider y be object such that
A1: [x,y] in Y|`f by XTUPLE_0:def 12;
y in Y & [x,y] in f by A1,RELAT_1:def 12;
hence x in f"Y by RELAT_1:def 14;
end;
assume x in f"Y;
then consider y be object such that
A2: [x,y] in f & y in Y by RELAT_1:def 14;
[x,y] in Y|`f by A2,RELAT_1:def 12;
hence x in dom(Y|`f) by XTUPLE_0:def 12;
end;
hence dom(Y|`f) = f"Y by TARSKI:2;
end;
theorem Th2:
for f being Function, Y1,Y2 being set st Y2 c= Y1 holds (Y1|`f)"Y2 = f"Y2
proof
let f be Function;
let Y1,Y2 be set;
assume
A1: Y2 c= Y1;
for x being object holds x in (Y1|`f)"Y2 iff x in f"Y2
proof
let x be object;
hereby
assume x in (Y1|`f)"Y2;
then consider y be object such that
A2: [x,y] in Y1|`f & y in Y2 by RELAT_1:def 14;
[x,y] in f by A2,RELAT_1:def 12;
hence x in f"Y2 by A2,RELAT_1:def 14;
end;
assume x in f"Y2;
then consider y be object such that
A3: [x,y] in f & y in Y2 by RELAT_1:def 14;
[x,y] in Y1|`f by A3,A1,RELAT_1:def 12;
hence x in (Y1|`f)"Y2 by A3,RELAT_1:def 14;
end;
hence (Y1|`f)"Y2 = f"Y2 by TARSKI:2;
end;
:: generalization TOPS_2 Th70
theorem Th3:
for S,T being TopStruct, f being Function of S,T holds
f is being_homeomorphism implies f" is being_homeomorphism
proof
let S, T be TopStruct;
let f be Function of S, T;
assume
A1: f is being_homeomorphism;
then
A2: dom f = [#]S & rng f = [#]T & f is one-to-one &
f is continuous & f" is continuous by TOPS_2:def 5;
per cases;
suppose S is non empty & T is non empty;
hence f" is being_homeomorphism by A1,TOPS_2:56;
end;
suppose A3: S is empty or T is empty;
A4: f = {}
proof
per cases by A3;
suppose S is empty; hence thesis; end;
suppose T is empty; hence thesis; end;
end;
reconsider g = f as onto one-to-one PartFunc of {},{} by A4,FUNCTOR0:1;
A5: f" = g" by A2;
A6: dom(f") = [#]T & rng(f") = [#]S by A2,A4;
reconsider g1 = f" as onto one-to-one PartFunc of {},{} by A5;
(f")" = g1" by A2,A4;
hence thesis by A4,A6,A2,TOPS_2:def 5;
end;
end;
definition
let S,T be TopStruct;
redefine pred S,T are_homeomorphic; :: redefines are_homeomorphic (T_0TOPSP, definition)
symmetry
proof
let S,T be TopStruct;
assume S,T are_homeomorphic;
then consider f be Function of S,T such that
A1: f is being_homeomorphism by T_0TOPSP:def 1;
f" is being_homeomorphism by A1,Th3;
hence thesis by T_0TOPSP:def 1;
end;
end;
reserve T1,T2,T3 for TopSpace,
A1 for Subset of T1, A2 for Subset of T2, A3 for Subset of T3;
:: like METRIZTS
theorem Th4:
for f be Function of T1,T2 st f is being_homeomorphism
for g be Function of T1|f"A2,T2|A2 st g = A2|`f
holds g is being_homeomorphism
proof
let f be Function of T1,T2 such that
A1: f is being_homeomorphism;
A2: dom f=[#]T1 & rng f=[#]T2 by A1,TOPS_2:def 5;
T1,T2 are_homeomorphic by A1,T_0TOPSP:def 1;
then T1 is empty iff T2 is empty by YELLOW14:18;
then
A3: [#]T1={} iff [#]T2={};
A4: rng f=[#]T2 by A1,TOPS_2:def 5;
set A= f"A2;
let g be Function of T1|A,T2|A2 such that
A5: g = A2|`f;
A6: rng g = A2 by A2,A5,RELAT_1:89;
A7: f is one-to-one by A1,TOPS_2:def 5;
then
A8: g is one-to-one by A5,FUNCT_1:58;
set TA=T1|A,TB=T2|A2;
A10: [#]TA=A by PRE_TOPC:def 5;
A11: [#]TA={} iff [#]TB={} by A6;
A12: [#]TB = A2 by PRE_TOPC:def 5;
A13: f is continuous by A1,TOPS_2:def 5;
for P be Subset of TB st P is open holds g"P is open
proof
let P be Subset of TB;
assume P is open;
then consider P1 be Subset of T2 such that
A14: P1 is open and
A15: P=P1/\A2 by A12,TSP_1:def 1;
A16: f"P1 is open by A3,A13,A14,TOPS_2:43;
g"P = f"P by A5,Th2,A15,XBOOLE_1:17
.= f"P1 /\ the carrier of TA by A10,A15,FUNCT_1:68;
hence thesis by A16,TSP_1:def 1;
end;
then
A17: g is continuous by A11,TOPS_2:43;
A18: f" is continuous by A1,TOPS_2:def 5;
for P be Subset of TA st P is open holds(g")"P is open
proof
let P be Subset of TA;
assume P is open;
then consider P1 be Subset of T1 such that
A19: P1 is open and
A20: P=P1/\A by A10,TSP_1:def 1;
A21: (f")"P1 is open by A3,A18,A19,TOPS_2:43;
A2 = f.:(f"A2) by A2,FUNCT_1:77; then
A22: the carrier of TB = (f")"A by A12,A4,A7,TOPS_2:54;
(g")"P = (A2|`f).:P by A5,A6,A8,A12,TOPS_2:54
.= f.:P /\ the carrier of TB by A12,FUNCT_1:67
.= (f")"(P1/\A) /\ the carrier of TB by A4,A7,A20,TOPS_2:54
.= (f")"P1 /\ (f")"A /\ the carrier of TB by FUNCT_1:68
.= (f")"P1 /\ ((f")"A /\ the carrier of TB) by XBOOLE_1:16
.= (f")"P1 /\ the carrier of TB by A22;
hence thesis by A21,TSP_1:def 1;
end;
then g" is continuous by A11,TOPS_2:43;
hence thesis by A6,A5,Th1,A10,A8,A12,A17,TOPS_2:def 5;
end;
theorem
for f be Function of T1,T2 st f is being_homeomorphism holds
f"A2,A2 are_homeomorphic
proof
let f be Function of T1,T2 such that
A1: f is being_homeomorphism;
A2: dom(A2|`f) = f"A2 by Th1
.= [#](T1|f"A2) by PRE_TOPC:def 5;
rng f = [#]T2 by A1,TOPS_2:def 5;
then rng(A2|`f) = A2 by RELAT_1:89
.= [#](T2|A2) by PRE_TOPC:def 5;
then reconsider g=A2|`f as Function of T1|f"A2,T2|A2 by A2,FUNCT_2:1;
g is being_homeomorphism by A1,Th4;
hence thesis by T_0TOPSP:def 1,METRIZTS:def 1;
end;
theorem
A1,A2 are_homeomorphic implies A2,A1 are_homeomorphic
proof
assume A1,A2 are_homeomorphic;
then T1|A1,T2|A2 are_homeomorphic by METRIZTS:def 1;
hence A2,A1 are_homeomorphic by METRIZTS:def 1;
end;
theorem Th7:
A1,A2 are_homeomorphic implies (A1 is empty iff A2 is empty)
proof
assume A1,A2 are_homeomorphic;
then consider f be Function of T1|A1,T2|A2 such that
A1: f is being_homeomorphism by METRIZTS:def 1,T_0TOPSP:def 1;
dom f = [#](T1|A1) & rng f = [#](T2|A2) & f is one-to-one &
f is continuous & f" is continuous by A1,TOPS_2:def 5;
hence thesis by PRE_TOPC:def 5;
end;
theorem
A1,A2 are_homeomorphic & A2,A3 are_homeomorphic
implies A1,A3 are_homeomorphic
proof
assume
A1: A1,A2 are_homeomorphic; then
A2: T1|A1,T2|A2 are_homeomorphic by METRIZTS:def 1;
assume A3: A2,A3 are_homeomorphic; then
A4: T2|A2,T3|A3 are_homeomorphic by METRIZTS:def 1;
per cases;
suppose A5: A2 is non empty; then
A6: A1 is non empty & A3 is non empty by A1,A3,Th7;
T1 is non empty & T2 is non empty & T3 is non empty by A5,A1,A3,Th7;
hence A1,A3 are_homeomorphic by A2,A4,A6,A5,BORSUK_3:3,METRIZTS:def 1;
end;
suppose A2 is empty;
then
A7: A1 is empty & A3 is empty by A1,A3,Th7;
reconsider f = {} as Function;
A8: the carrier of T1|A1 = {} & the carrier of T3|A3 = {} by A7;
dom f = {} & rng f = {};
then reconsider f as Function of T1|A1,T3|A3 by A8,FUNCT_2:1;
A9: dom f = [#](T1|A1) & rng f = [#](T3|A3) by A8;
for P1 being Subset of T3|A3 st P1 is closed holds f"P1 is closed;
then
A10: f is continuous by PRE_TOPC:def 6;
reconsider g = f as onto one-to-one PartFunc of {},{} by FUNCTOR0:1;
for P1 being Subset of T1|A1 st P1 is closed holds (f")"P1 is closed by A7;
then f" is continuous by PRE_TOPC:def 6;
then f is being_homeomorphism by A9,A10,TOPS_2:def 5;
hence thesis by METRIZTS:def 1,T_0TOPSP:def 1;
end;
end;
theorem Th9:
T1 is second-countable & T1,T2 are_homeomorphic
implies T2 is second-countable
proof
assume T1 is second-countable;
then
A1: weight T1 c= omega by WAYBEL23:def 6;
assume T1,T2 are_homeomorphic;
then weight T1 = weight T2 by METRIZTS:4;
hence T2 is second-countable by A1,WAYBEL23:def 6;
end;
reserve n,k for Nat;
reserve M,N for non empty TopSpace;
theorem Th10:
M is Hausdorff & M,N are_homeomorphic implies N is Hausdorff
proof
assume
A1: M is Hausdorff;
assume M,N are_homeomorphic;
then consider f be Function of N,M such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
A3: dom f = [#]N & rng f = [#]M & f is one-to-one & f is continuous &
f" is continuous by A2,TOPS_2:def 5;
for p, q being Point of N st p <> q holds
ex N1, N2 being Subset of N st
N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2
proof
let p, q be Point of N;
assume p <> q;
then consider M1, M2 be Subset of M such that
A4: M1 is open & M2 is open & f.p in M1 & f.q in M2 & M1 misses M2
by A1,A3,PRE_TOPC:def 10;
reconsider N1 = f"M1 as Subset of N;
reconsider N2 = f"M2 as Subset of N;
take N1, N2;
thus N1 is open & N2 is open by A4,A3,TOPS_2:43;
thus p in N1 & q in N2 by A4,FUNCT_2:38;
thus N1 misses N2 by A4,FUNCT_1:71;
end;
hence N is Hausdorff by PRE_TOPC:def 10;
end;
::$CT
:: see MFOLD_0:10,11
theorem Th12:
M is n-manifold & M,N are_homeomorphic implies N is n-manifold
proof
assume
A1: M is n-manifold;
assume
A2: M,N are_homeomorphic;
then
A3: N is second-countable by A1,Th9;
A4: N is Hausdorff by A1,A2,Th10;
N is n-locally_euclidean by A1,A2,MFOLD_0:10,11;
hence N is n-manifold by A3,A4;
end;
:: like MATRIX14
theorem Th13:
for x1,x2 being FinSequence of REAL,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
let x1,x2 be FinSequence of REAL,
i be Element of NAT;
assume
A1: i in dom mlt(x1,x2);
A2: mlt(x1,x2)= multreal.:(x1,x2) by RVSUM_1:def 9;
dom multreal=[:REAL, REAL:] & rng x1 c= REAL by FUNCT_2:def 1;
then [:rng x1, rng x2:] c= dom multreal by ZFMISC_1:96;
then
A3: dom mlt(x1,x2) = dom x1 /\ dom x2 by A2,FUNCOP_1:69;
then i in dom x2 by A1,XBOOLE_0:def 4;
then
A4: x2/.i=x2.i by PARTFUN1:def 6;
i in dom x1 by A1,A3,XBOOLE_0:def 4;
then x1/.i=x1.i by PARTFUN1:def 6;
hence mlt(x1,x2).i = (x1/.i)*(x2/.i) by A4,RVSUM_1:59;
hence thesis by A1,PARTFUN1:def 6;
end;
theorem Th14:
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
let x1,x2,y1,y2 be FinSequence of REAL;
assume that
A1: len x1=len x2 and
A2: len y1=len y2;
A3: multreal .:(x1^y1,x2^y2)=multreal * (<: x1^y1,x2^y2 :>)
by FUNCOP_1:def 3;
A4: dom (x1^y1)=Seg len (x1^y1) by FINSEQ_1:def 3;
dom multreal = [:REAL, REAL:] & rng (x1^y1) c= REAL by FUNCT_2:def 1;
then [:rng (x1^y1), rng (x2^y2):] c= dom multreal by ZFMISC_1:96;
then
A5: dom (multreal * (<: x1^y1,x2^y2 :>)) =dom (x1^y1) /\ dom (x2^y2)
by A3,FUNCOP_1:69;
A6: len (x2^y2)=len x2+len y2 by FINSEQ_1:22;
then dom (x1^y1)=dom (x2^y2) by A1,A2,A4,FINSEQ_1:22,def 3;
then
A7: dom (mlt(x1^y1,x2^y2))= dom (x1^y1) by A3,A5,RVSUM_1:def 9;
A8: multreal.:(y1,y2)=multreal * (<:y1,y2:>) by FUNCOP_1:def 3;
A9: dom multreal = [:REAL, REAL:] by FUNCT_2:def 1;
then [:rng y1, rng y2:] c= dom multreal by ZFMISC_1:96;
then
A10: dom (multreal * (<:y1,y2:>)) =dom y1 /\ dom y2 by A8,FUNCOP_1:69;
dom y2=Seg len y1 by A2,FINSEQ_1:def 3
.=dom y1 by FINSEQ_1:def 3;
then
A11: dom mlt(y1,y2) =dom y1 by A8,A10,RVSUM_1:def 9;
then dom (mlt(y1,y2))=Seg len y1 by FINSEQ_1:def 3;
then
A12: len (mlt(y1,y2))= len y1 by FINSEQ_1:def 3;
A13: multreal.:(x1,x2)=multreal * (<:x1,x2:>) by FUNCOP_1:def 3;
[:rng (x1), rng (x2):] c= dom multreal by A9,ZFMISC_1:96;
then
A14: dom (multreal * (<:x1,x2:>)) =dom (x1) /\ dom (x2) by A13,FUNCOP_1:69;
A15: len (x1^y1)=len x1+len y1 by FINSEQ_1:22;
dom x2=Seg len x1 by A1,FINSEQ_1:def 3
.=dom x1 by FINSEQ_1:def 3;
then
A16: dom (mlt(x1,x2)) =dom x1 by A13,A14,RVSUM_1:def 9;
then
A17: dom (mlt(x1,x2))=Seg len x1 by FINSEQ_1:def 3;
A18: for i being Nat st 1<=i & i<=len (mlt(x1^y1,x2^y2)) holds (mlt(x1^y1,x2
^y2)).i=((mlt(x1,x2))^(mlt(y1,y2))).i
proof
let i be Nat;
assume that
A19: 1<=i and
A20: i<=len (mlt(x1^y1,x2^y2));
i in Seg len (mlt(x1^y1,x2^y2)) by A19,A20;
then
A21: i in dom (mlt(x1^y1,x2^y2)) by FINSEQ_1:def 3;
then i<=len (x1^y1) by A4,A7,FINSEQ_1:1;
then
A22: (x1^y1)/.i= (x1^y1).i by A19,FINSEQ_4:15;
i<=len (x2^y2) by A1,A2,A15,A6,A4,A7,A21,FINSEQ_1:1;
then
A23: (x2^y2)/.i= (x2^y2).i by A19,FINSEQ_4:15;
A24: i<=len x1+len y1 by A15,A4,A7,A21,FINSEQ_1:1;
now
per cases;
suppose
A25: i<=len x1;
then
A26: i in Seg len x1 by A19;
then
A27: i in dom x1 by FINSEQ_1:def 3;
i in dom x2 by A1,A26,FINSEQ_1:def 3;
then
A28: (x2^y2).i=x2.i by FINSEQ_1:def 7;
A29: i in dom (mlt(x1,x2)) by A16,A26,FINSEQ_1:def 3;
then
A30: ((mlt(x1,x2))^(mlt(y1,y2))).i =(mlt(x1,x2)).i by FINSEQ_1:def 7
.=(x1/.i)*(x2/.i) by A29,Th13;
x1/.i=x1.i & x2/.i=x2.i by A1,A19,A25,FINSEQ_4:15;
hence ((x1^y1)/.i)*((x2^y2)/.i)=((mlt(x1,x2))^(mlt(y1,y2))).i
by A22,A23,A27,A28,A30,FINSEQ_1:def 7;
end;
suppose
A31: i>len x1;
i<=len (x2^y2) by A1,A2,A15,A6,A4,A7,A21,FINSEQ_1:1;
then
A32: (x2^y2)/.i= (x2^y2).i by A19,FINSEQ_4:15;
i<=len (x1^y1) by A4,A7,A21,FINSEQ_1:1;
then
A33: (x1^y1)/.i= (x1^y1).i by A19,FINSEQ_4:15;
set k=i -' len x1;
A34: k=i-len x1 by A31,XREAL_1:233;
then
A35: i= len x1 +k;
i-len x1 <=len x1 + len y1 - len x1 by A24,XREAL_1:13;
then
A36: k<=len y1 by A31,XREAL_1:233;
k>0 by A31,A34,XREAL_1:50;
then k+1>0+1 by XREAL_1:6;
then
A37: 1<=k by NAT_1:13;
then
A38: k in Seg len y1 by A36;
then
A39: k in dom (mlt(y1,y2)) by A11,FINSEQ_1:def 3;
i=len (mlt(x1,x2)) +k by A17,A35,FINSEQ_1:def 3;
then
A40: ((mlt(x1,x2))^(mlt(y1,y2))).i =(mlt(y1,y2)).k by A39,FINSEQ_1:def 7
.=(y1/.k)*(y2/.k) by A39,Th13;
k in dom y1 by A38,FINSEQ_1:def 3;
then
A41: (x1^y1).i=y1.k by A35,FINSEQ_1:def 7;
k in Seg len y1 by A37,A36;
then
A42: k in dom y2 by A2,FINSEQ_1:def 3;
y1/.k=y1.k & y2/.k=y2.k by A2,A37,A36,FINSEQ_4:15;
hence ((x1^y1)/.i)*((x2^y2)/.i)=((mlt(x1,x2))^(mlt(y1,y2))).i
by A1,A35,A42,A41,A33,A32,A40,FINSEQ_1:def 7;
end;
end;
hence thesis by A21,Th13;
end;
len (mlt(x1^y1,x2^y2))=len (x1^y1) by A4,A7,FINSEQ_1:def 3
.=len x1 + len y1 by FINSEQ_1:22;
then len (mlt(x1^y1,x2^y2)) =len (mlt(x1,x2))+ len(mlt(y1,y2)) by A17,A12,
FINSEQ_1:def 3;
hence thesis by A18,FINSEQ_1:22;
end;
theorem Th15:
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
let x1,x2,y1,y2 be FinSequence of REAL;
A1: Sum ((mlt(x1,x2))^(mlt(y1,y2)))=Sum mlt(x1,x2) + Sum mlt(y1,y2) by
RVSUM_1:75;
assume len x1=len x2 & len y1=len y2;
then Sum mlt(x1^y1,x2^y2) = Sum mlt(x1,x2) + Sum mlt(y1,y2) by A1,Th14;
then |( x1^y1, x2^y2 )| = Sum mlt(x1,x2) + Sum mlt(y1,y2) by RVSUM_1:def 16;
then |( x1^y1, x2^y2 )| = Sum mlt(x1,x2) + |(y1,y2)| by RVSUM_1:def 16;
hence thesis by RVSUM_1:def 16;
end;
Lm1:
the carrier of RealVectSpace(Seg n) = the carrier of TOP-REAL n
proof
reconsider D = REAL as non empty set;
A1: Funcs(Seg n,D) = REAL n by FINSEQ_2:93;
RealVectSpace(Seg n) =
RLSStruct(# Funcs(Seg n,REAL),RealFuncZero Seg n,
RealFuncAdd Seg n,RealFuncExtMult Seg n #) by FUNCSDOM:def 6;
hence thesis by A1,EUCLID:22;
end;
Lm2: 0.RealVectSpace(Seg n) = 0.(TOP-REAL n)
proof
RealVectSpace(Seg n) =
RLSStruct(# Funcs(Seg n,REAL),RealFuncZero Seg n,
RealFuncAdd Seg n,RealFuncExtMult Seg n #) by FUNCSDOM:def 6;
hence 0.RealVectSpace(Seg n) = Seg n --> 0 by FUNCSDOM:def 4
.= 0*n by FINSEQ_2:def 2
.= 0.(TOP-REAL n) by EUCLID:70;
end;
reserve p,q,p1,p2 for Point of TOP-REAL n;
reserve r for Real;
theorem Th16:
k in Seg n implies (p1+p2).k = p1.k + p2.k
proof
A1: dom(p1+p2) = Seg n by FINSEQ_1:89;
thus thesis by A1,VALUED_1:def 1;
end;
:: like MATRTOP_2
theorem Th17:
for X being set holds
X is Linear_Combination of RealVectSpace(Seg n)
iff
X is Linear_Combination of TOP-REAL n
proof
let X be set;
set V=RealVectSpace(Seg n);
set T=TOP-REAL n;
hereby assume X is Linear_Combination of V;
then reconsider L=X as Linear_Combination of V;
consider S be finite Subset of V such that
A1: for v be Element of V st not v in S holds L.v = 0
by RLVECT_2:def 3;
A2: now let v be Element of T;
assume A3: not v in S;
v is Element of V by Lm1;
hence 0=L.v by A1,A3;
end;
(L is Element of Funcs(the carrier of T,REAL)) & S is finite Subset of T
by Lm1;
hence X is Linear_Combination of T by A2,RLVECT_2:def 3;
end;
assume X is Linear_Combination of T;
then reconsider L=X as Linear_Combination of T;
consider S be finite Subset of T such that
A4: for v be Element of T st not v in S holds L.v=0 by RLVECT_2:def 3;
A5: now let v be Element of V;
assume
A6: not v in S;
v is Element of T by Lm1;
hence 0=L.v by A4,A6;
end;
L is Element of Funcs(the carrier of V,REAL) &
S is finite Subset of V by Lm1;
hence thesis by A5,RLVECT_2:def 3;
end;
theorem Th18:
for F be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of RealVectSpace(Seg n),
fv be Function of RealVectSpace(Seg n),REAL st fr = fv & F = Fv
holds fr(#)F = fv(#)Fv
proof
let F be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of RealVectSpace(Seg n),
fv be Function of RealVectSpace(Seg n),REAL;
assume that
A1: fr=fv and
A2: F=Fv;
A3: len(fv(#)Fv)=len Fv by RLVECT_2:def 7;
A4: len(fr(#)F)=len F by RLVECT_2:def 7;
now reconsider T=TOP-REAL n as RealLinearSpace;
let i be Nat;
reconsider Fi=F/.i as FinSequence of REAL by EUCLID:24;
A5: the carrier of n-VectSp_over F_Real=the carrier of TOP-REAL n
proof
thus the carrier of n-VectSp_over F_Real=REAL n by MATRIX13:102
.=the carrier of TOP-REAL n by EUCLID:22;
end;
the carrier of n -VectSp_over F_Real
= n-tuples_on the carrier of F_Real by MATRIX13:102;
then reconsider Fvi=Fv/.i as Element of n-tuples_on the carrier of F_Real
by Lm1,A5;
reconsider Fii=F/.i as Element of T;
assume
A6: 1<=i & i<=len F;
then
A7: i in dom(fv(#)Fv) by A2,A3,FINSEQ_3:25;
i in dom F by A6,FINSEQ_3:25;
then
A8: F/.i=F.i by PARTFUN1:def 6;
A9: Fv/.i=Fv.i by A2,A6,FINSEQ_3:25,PARTFUN1:def 6;
i in dom(fr(#)F) by A4,A6,FINSEQ_3:25;
hence (fr(#)F).i=fr.Fii*Fii by RLVECT_2:def 7
.=fv.(Fv/.i)*(Fv/.i) by A1,A2,A8,A9,EUCLID:65
.=(fv(#)Fv).i by A7,RLVECT_2:def 7;
end;
hence thesis by A2,A4,RLVECT_2:def 7;
end;
theorem Th19:
for F be FinSequence of TOP-REAL n,
Fv be FinSequence of RealVectSpace(Seg n) st Fv = F
holds Sum F = Sum Fv
proof
set T=TOP-REAL n;
set V=RealVectSpace(Seg n);
let F be FinSequence of T;
let Fv be FinSequence of V such that
A1: Fv=F;
reconsider T=TOP-REAL n as RealLinearSpace;
consider f be sequence of the carrier of T such that
A2: Sum F=f.(len F) and
A3: f.0=0.T and
A4: for j be Nat,v be Element of T st j<len F & v=F.(j+1)
holds f.(j+1)=f.j+v by RLVECT_1:def 12;
consider fv be sequence of the carrier of V such that
A5: Sum Fv=fv.(len Fv) and
A6: fv.0=0.V and
A7: for j be Nat,v be Element of V st j<len Fv & v=Fv.(j+1)
holds fv.(j+1)=fv.j+v by RLVECT_1:def 12;
defpred P[Nat] means $1<=len F implies f.$1=fv.$1;
A8: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A9: P[i];
set i1=i+1;
A10: the carrier of n-VectSp_over F_Real=the carrier of TOP-REAL n
proof
thus the carrier of n-VectSp_over F_Real=REAL n by MATRIX13:102
.=the carrier of TOP-REAL n by EUCLID:22;
end;
the carrier of n -VectSp_over F_Real
= n-tuples_on the carrier of F_Real by MATRIX13:102;
then reconsider Fvi1=Fv/.i1,fvi=fv.i as Element of n-tuples_on
the carrier of F_Real by A10,Lm1;
reconsider Fi1=F/.i1 as Element of T;
assume
A11: i1<=len F;
A13: i1 in dom F by A11,NAT_1:11,FINSEQ_3:25;
then F.i1=F/.i1 by PARTFUN1:def 6;
then A14: f.i1=f.i+Fi1 by A4,A11,NAT_1:13;
A15: Fv/.i1=Fv.i1 by A1,A13,PARTFUN1:def 6;
then Fvi1 = F/.i1 by A1,A13,PARTFUN1:def 6;
hence f.i1 = fv.i+Fv/.i1 by A9,A11,A14,EUCLID:64,NAT_1:13
.=fv.i1 by A1,A7,A11, NAT_1:13,A15;
end;
A16: P[0] by A3,A6,Lm2;
for n be Nat holds P[n] from NAT_1:sch 2(A16,A8);
hence thesis by A1,A2,A5;
end;
theorem Th20:
for Lv be Linear_Combination of RealVectSpace(Seg n),
Lr be Linear_Combination of TOP-REAL n st Lr = Lv
holds Sum Lr = Sum Lv
proof
set V=RealVectSpace(Seg n);
set T=TOP-REAL n;
let Lv be Linear_Combination of V;
let Lr be Linear_Combination of T such that
A1: Lr=Lv;
consider F be FinSequence of the carrier of T such that
A2: (F is one-to-one) & rng F=Carrier(Lr) and
A3: Sum Lr=Sum(Lr(#)F) by RLVECT_2:def 8;
reconsider F1=F as FinSequence of the carrier of V by Lm1;
A4: Lr(#)F=Lv(#)F1 by A1,Th18;
thus Sum Lv=Sum(Lv(#)F1) by A1,A2,RLVECT_2:def 8
.=Sum Lr by A3,A4,Th19;
end;
theorem Th21:
for Af be Subset of RealVectSpace(Seg n),
Ar be Subset of TOP-REAL n st Af = Ar
holds Af is linearly-independent iff Ar is linearly-independent
proof
set V=RealVectSpace(Seg n);
let AV be Subset of V;
set T=TOP-REAL n;
let AR be Subset of T such that
A1: AV=AR;
hereby
assume
A2: AV is linearly-independent;
now let L be Linear_Combination of AR;
reconsider L1=L as Linear_Combination of V by Th17;
assume Sum L=0.T;
then
A3: 0.V=Sum L by Lm2 .=Sum L1 by Th20;
Carrier L c=AR by RLVECT_2:def 6;
then L1 is Linear_Combination of AV by A1,RLVECT_2:def 6;
hence Carrier L={} by A2,A3,RLVECT_3:def 1;
end;
hence AR is linearly-independent by RLVECT_3:def 1;
end;
assume
A4: AR is linearly-independent;
now let L be Linear_Combination of AV;
reconsider L1=L as Linear_Combination of T by Th17;
Carrier L c=AV by RLVECT_2:def 6;
then reconsider L1 as Linear_Combination of AR by A1,RLVECT_2:def 6;
assume Sum L=0.V;
then 0.T=Sum L by Lm2 .=Sum L1 by Th20;
hence Carrier L={} by A4,RLVECT_3:def 1;
end;
hence thesis by RLVECT_3:def 1;
end;
theorem Th22:
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
let V be Subset of TOP-REAL n;
assume
A1: V = RN_Base n;
reconsider p0 = p as Element of RealVectSpace(Seg n) by Lm1;
reconsider V0 = V as Subset of RealVectSpace(Seg n) by Lm1;
consider l0 be Linear_Combination of V0 such that
A2: p0 = Sum l0 by A1,EUCLID_7:43;
reconsider l=l0 as Linear_Combination of TOP-REAL n by Th17;
Carrier l0 c= V0 by RLVECT_2:def 6;
then reconsider l as Linear_Combination of V by RLVECT_2:def 6;
take l;
thus p = Sum l by A2,Th20;
end;
theorem
RN_Base n is Basis of TOP-REAL n
proof
set A = RN_Base n;
set T = TOP-REAL n;
RN_Base n c= REAL n;
then A1: RN_Base n c= the carrier of T by EUCLID:22;
reconsider A as finite Subset of T by EUCLID:22;
reconsider B = RN_Base n as Subset of RealVectSpace(Seg n) by A1,Lm1;
B is Basis of RealVectSpace(Seg n) by EUCLID_7:45;
then B is linearly-independent by RLVECT_3:def 3;
then A2: A is linearly-independent by Th21;
reconsider V1 = (Omega).T as RealLinearSpace;
for v being VECTOR of T st v in Lin A holds v in V1
proof
let v be VECTOR of T;
assume v in Lin A;
v in the RLSStruct of T;
hence v in V1 by RLSUB_1:def 4;
end;
then reconsider X = Lin A as Subspace of V1 by RLSUB_1:29;
for x being object holds x in the carrier of X iff x in the carrier of V1
proof
let x be object;
hereby
assume x in the carrier of X;
then x in X;
then x in V1 by RLSUB_1:9;
hence x in the carrier of V1;
end;
assume x in the carrier of V1;
then x in the RLSStruct of T by RLSUB_1:def 4;
then reconsider x0 = x as Element of TOP-REAL n;
ex l being Linear_Combination of A st x0 = Sum l by Th22;
then x in the set of all Sum l where l is Linear_Combination of A;
hence x in the carrier of X by RLVECT_3:def 2;
end;
then Lin A = (Omega).T by TARSKI:2,EUCLID_7:9;
then Lin A = the RLSStruct of T by RLSUB_1:def 4;
hence RN_Base n is Basis of T by A2,RLVECT_3:def 3;
end;
theorem Th24:
for V being Subset of TOP-REAL n holds
V in the topology of TOP-REAL n iff
for p st p in V ex r st r > 0 & Ball(p,r) c= V
proof
let V be Subset of TOP-REAL n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
set T = TOP-REAL n;
A1: the TopStruct of T = TopSpaceMetr Euclid n by EUCLID:def 8;
A2: TopSpaceMetr Euclid n = TopStruct (#the carrier of Euclid n,
Family_open_set Euclid n#) by PCOMPS_1:def 5;
reconsider V1 = V as Subset of Euclid n by EUCLID:67;
hereby
assume
A3: V in the topology of T;
let p;
assume
A4: p in V;
reconsider x = p as Element of Euclid n by EUCLID:67;
consider r be Real such that
A5: r > 0 & Ball(x,r) c= V1 by A3,A4,A1,A2,PCOMPS_1:def 4;
reconsider r as Real;
take r;
thus r > 0 by A5;
reconsider x1 = x as Point of Euclid n1;
reconsider p1 = p as Point of TOP-REAL n1;
thus Ball(p,r) c= V by A5,TOPREAL9:13;
end;
assume
A6: for p st p in V holds ex r being Real st r > 0 & Ball(p,r) c= V;
for x being Element of Euclid n st x in V1 holds
ex r being Real st r > 0 & Ball(x,r) c= V1
proof
let x be Element of Euclid n;
assume
A7: x in V1;
reconsider p = x as Point of T by EUCLID:67;
consider r be Real such that
A8: r > 0 & Ball(p,r) c= V by A6,A7;
take r;
thus r > 0 by A8;
reconsider x1 = x as Point of Euclid n1;
reconsider p1 = p as Point of TOP-REAL n1;
thus Ball(x,r) c= V1 by A8,TOPREAL9:13;
end;
hence V in the topology of T by A1,A2,PCOMPS_1:def 4;
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:
for q being Point of TOP-REAL n holds it.q = |(p,q)|;
existence
proof
defpred P[object,object] means ex q being Point of TOP-REAL n
st q=$1 & $2=|(p,q)|;
A1: for x being object st x in the carrier of TOP-REAL n
ex y being object st P[x,y]
proof
let x be object;
assume x in the carrier of TOP-REAL n;
then reconsider q3=x as Point of TOP-REAL n;
take |(p,q3)|;
thus thesis;
end;
consider f1 being Function such that
A2: dom f1 = (the carrier of TOP-REAL n) & for x being object
st x in (the carrier of
TOP-REAL n) holds P[x,f1.x] from CLASSES1:sch 1(A1);
rng f1 c= the carrier of R^1
proof
let z be object;
assume z in rng f1;
then consider xz being object such that
A3: xz in dom f1 and
A4: z=f1.xz by FUNCT_1:def 3;
ex q4 be Point of TOP-REAL n st q4=xz & f1.xz=|(p,q4)| by A2,A3;
hence thesis by A4,TOPMETR:17,XREAL_0:def 1;
end;
then reconsider f2=f1 as Function of TOP-REAL n,R^1
by A2,FUNCT_2:def 1,RELSET_1:4;
take f2;
for q being Point of TOP-REAL n holds f1.q=|(p,q)|
proof
let q be Point of TOP-REAL n;
ex q2 being Point of TOP-REAL n st q2=q & f1.q=|(p,q2)| by A2;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of TOP-REAL n,R^1 such that
A6: for q being Point of TOP-REAL n holds f1.q = |(p,q)| and
A7: for q being Point of TOP-REAL n holds f2.q = |(p,q)|;
for q being Point of TOP-REAL n holds f1.q = f2.q
proof
let q be Point of TOP-REAL n;
thus f1.q = |(p,q)| by A6 .= f2.q by A7;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
let n,p;
cluster InnerProduct(p) -> continuous;
correctness
proof
set f = InnerProduct(p);
A1: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider
f1=f as Function of TopSpaceMetr(Euclid n),TopSpaceMetr(RealSpace)
by TOPMETR:def 6;
per cases;
suppose
A2: p = 0.TOP-REAL n;
A3: for q being Point of TOP-REAL n holds f.q = 0
proof
let q be Point of TOP-REAL n;
f.q = |(q,p)| by Def1;
hence thesis by A2,EUCLID_2:32;
end;
consider g be Function of TOP-REAL n,R^1 such that
A4: (for p being Point of TOP-REAL n holds g.p = 0) & g is continuous
by JGRAPH_2:20;
for x being object st x in the carrier of TOP-REAL n holds f.x = g.x
proof
let x be object;
assume x in the carrier of TOP-REAL n;
then reconsider q=x as Point of TOP-REAL n;
thus f.x = f.q .= 0 by A3 .= g.q by A4 .= g.x;
end;
hence thesis by A4,FUNCT_2:12;
end;
suppose p <> 0.TOP-REAL n;
then
A5: |.p.| > 0 by EUCLID_2:44;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
now
let r be Real,u be Element of Euclid n,u1 be Element
of RealSpace;
assume that
A6: r>0 and
A7: u1=f1.u;
set s1 = r / |.p.|;
for w being Element of Euclid n, w1 being Element of RealSpace st w1=
f1.w & dist(u,w)<s1 holds dist(u1,w1)<r
proof
let w be Element of Euclid n, w1 be Element of RealSpace;
assume that
A8: w1=f1.w and
A9: dist(u,w)<s1;
reconsider tu=u1,tw=w1 as Real by METRIC_1:def 13;
reconsider qw=w,qu=u as Point of TOP-REAL n1 by TOPREAL3:8;
A10: dist(u1,w1)=(the distance of RealSpace).(u1,w1) by METRIC_1:def 1
.=|.tu-tw.| by METRIC_1:def 12,def 13;
A11: w1=|(qw,p)| by Def1,A8;
|.tu-tw.| = |.|(qu,p)|-|(qw,p)|.| by Def1,A7,A11
.= |.|(qu - qw,p)|.| by EUCLID_2:24;
then
A12: dist(u1,w1) <= |.qu-qw.|*|.p.| by A10,EUCLID_2:51;
A13: dist(u,w)*|.p.|=|.qu-qw.|*|.p.| by JGRAPH_1:28;
dist(u,w)*|.p.| < r/|.p.|*|.p.| by A9,A5,XREAL_1:68;
then dist(u,w)*|.p.| < r/(|.p.|/|.p.|) by XCMPLX_1:82;
then dist(u,w)*|.p.| < r/1 by A5,XCMPLX_1:60;
hence thesis by A13,A12,XXREAL_0:2;
end;
hence ex s being Real st s>0 &
for w being Element of Euclid n, w1
being Element of RealSpace st w1=f1.w & dist(u,w)<s
holds dist(u1,w1)<r by A5,A6;
end;
then f1 is continuous by UNIFORM1:3;
hence thesis by A1,PRE_TOPC:32,TOPMETR:def 6;
end;
end;
end;
begin :: Planes
definition
let n;
let p,q;
func Plane(p,q) -> Subset of TOP-REAL n equals
{y where y is Point of TOP-REAL n: |( p,y-q )| = 0 };
correctness
proof
set X = {y where y is Point of TOP-REAL n: |( p,y-q )| = 0 };
now
let x be object;
assume x in X;
then consider y be Point of TOP-REAL n such that
A1: x = y & |( p,y-q )| = 0;
thus x in the carrier of TOP-REAL n by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th25:
transl(p1,TOP-REAL n) .: Plane(p,p2) = Plane(p,p1+p2)
proof
A1: now
let y be object;
assume y in transl(p1,TOP-REAL n) .: Plane(p,p2);
then consider x be object such that
A2: [x,y] in transl(p1,TOP-REAL n) & x in Plane(p,p2) by RELAT_1:def 13;
consider x1 be Point of TOP-REAL n such that
A3: x = x1 & |( p,x1-p2 )| = 0 by A2;
A4: y = transl(p1,TOP-REAL n).x1 by A2,A3,FUNCT_1:1
.= p1+x1 by RLTOPSP1:def 10;
x in dom transl(p1,TOP-REAL n) &
y = transl(p1,TOP-REAL n).x by A2,FUNCT_1:1;
then y in rng transl(p1,TOP-REAL n) by FUNCT_1:3;
then reconsider y1 = y as Point of TOP-REAL n;
x1-p2 = x1-p2+0.TOP-REAL n by RLVECT_1:4
.= x1-p2+(p1 + -p1) by RLVECT_1:5
.= x1 + -p2 +p1 + -p1 by RLVECT_1:def 3
.= y1 -p2 -p1 by A4,RLVECT_1:def 3
.= y1 -(p1+p2) by RLVECT_1:27;
hence y in Plane(p,p1+p2) by A3;
end;
now
let y be object;
assume y in Plane(p,p1+p2);
then consider y1 be Point of TOP-REAL n such that
A5: y = y1 & |( p,y1-(p1+p2) )| = 0;
set x = y1-p1;
x in the carrier of TOP-REAL n; then
A6: x in dom transl(p1,TOP-REAL n) by FUNCT_2:def 1;
p1 + x = y1 by RLVECT_4:1;
then transl(p1,TOP-REAL n).x = y1 by RLTOPSP1:def 10; then
A7: [x,y1] in transl(p1,TOP-REAL n) by A6,FUNCT_1:1;
x-p2 = y1 -(p1+p2) by RLVECT_1:27;
then x in Plane(p,p2) by A5;
hence y in transl(p1,TOP-REAL n) .: Plane(p,p2)
by A5,A7,RELAT_1:def 13;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th26:
p <> 0.TOP-REAL n implies
ex A being linearly-independent Subset of TOP-REAL n
st card A = n - 1 & [#]Lin(A) = Plane(p,0.TOP-REAL n)
proof
assume
A1: p <> 0.TOP-REAL n;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A2: 0.TOP-REAL n = -0.TOP-REAL n1 by JGRAPH_5:10
.= -0.TOP-REAL n;
set V1 = Plane(p,0.TOP-REAL n);
|( p,0.TOP-REAL n )| = 0 by EUCLID_2:32;
then |( p,0.TOP-REAL n-0.TOP-REAL n )| = 0 by RLVECT_1:5;
then
A3: 0.TOP-REAL n in V1;
A4: for v, u being VECTOR of TOP-REAL n st v in V1 & u in V1 holds v + u in V1
proof
let v, u be VECTOR of TOP-REAL n;
assume v in V1;
then consider v1 be Point of TOP-REAL n such that
A5: v = v1 & |( p,v1-0.TOP-REAL n )| = 0;
assume u in V1;
then consider u1 be Point of TOP-REAL n such that
A6: u = u1 & |( p,u1-0.TOP-REAL n )| = 0;
|( p,(v1+u1)-0.TOP-REAL n )| = |( p,v1+(u1-0.TOP-REAL n) )| by
RLVECT_1:def 3
.= |( p, v1 )| + |( p, u1-0.TOP-REAL n )| by EUCLID_2:26
.= 0 by A5,A2,A6,RLVECT_1:4;
hence v + u in V1 by A5,A6;
end;
for a being Real for v being VECTOR of TOP-REAL n st v in V1
holds a * v in V1
proof
let a be Real;
let v be VECTOR of TOP-REAL n;
assume v in V1;
then consider v1 be Point of TOP-REAL n such that
A7: v = v1 & |( p,v1-0.TOP-REAL n )| = 0;
|( p,a*(v1-0.TOP-REAL n) )| = a * (0 qua Real) by A7,EUCLID_2:20;
then |( p,a*v1 - a*0.TOP-REAL n )| = 0 by RLVECT_1:34;
then |( p, a*v1 - 0.TOP-REAL n )| = 0 by RLVECT_1:10;
hence a * v in V1 by A7;
end;
then consider W be strict Subspace of TOP-REAL n such that
A8: V1 = the carrier of W by A3,RLSUB_1:35,A4,RLSUB_1:def 1;
set A1 = the Basis of W;
A10: [#]Lin A1 = Plane(p,0.TOP-REAL n) by A8,RLVECT_3:def 3;
reconsider A = A1 as linearly-independent Subset of TOP-REAL n
by RLVECT_3:def 3,RLVECT_5:14;
take A;
reconsider A2 = {p} as linearly-independent Subset of TOP-REAL n
by A1,RLVECT_3:8;
A11: dim Lin A2 = card A2 by RLVECT_5:29 .= 1 by CARD_1:30;
for v being VECTOR of TOP-REAL n ex v1,v2 being VECTOR of TOP-REAL n
st v1 in Lin A & v2 in Lin A2 & v = v1 + v2
proof
let v be VECTOR of TOP-REAL n;
set a = |( p,v )| / |( p,p )|;
set v2 = a * p;
set v1 = v - v2;
reconsider v1,v2 as VECTOR of TOP-REAL n;
take v1,v2;
A12: |( p,p )| > 0 by A1,EUCLID_2:43;
|( p,v1 )| = |( p, v )| - |( p, v2 )| by EUCLID_2:27
.= |( p, v )| - a * |( p, p )| by EUCLID_2:20
.= |( p, v )| - |( p, v )| by A12,XCMPLX_1:87
.= 0;
then |( p,v1 - 0.TOP-REAL n )| = 0 by A2,RLVECT_1:4;
then v1 in Lin A1 by A10;
hence v1 in Lin A by RLVECT_5:20;
thus v2 in Lin A2 by RLVECT_4:8;
thus thesis by RLVECT_4:1;
end;
then
A13: the RLSStruct of TOP-REAL n = Lin(A) + Lin(A2) by RLSUB_2:44;
Lin(A) /\ Lin(A2) = (0).TOP-REAL n
proof
for v being VECTOR of TOP-REAL n holds
v in Lin(A) /\ Lin(A2) iff v in (0).TOP-REAL n
proof
let v be VECTOR of TOP-REAL n;
hereby
assume v in Lin(A) /\ Lin(A2);
then
A14: v in Lin(A) & v in Lin(A2) by RLSUB_2:3;
then consider a be Real such that
A15: v = a * p by RLVECT_4:8;
v in Plane(p,0.TOP-REAL n) by A10,A14,RLVECT_5:20;
then consider y be Point of TOP-REAL n such that
A16: y = v & |( p,y-0.TOP-REAL n )| = 0;
|( p,v )| = 0 by A2,A16,RLVECT_1:4;
then
A17: a * |( p,p )| = 0 by A15,EUCLID_2:20;
|( p,p )| > 0 by A1,EUCLID_2:43;
then a = 0 by A17;
then v = 0.TOP-REAL n by A15,RLVECT_1:10;
hence v in (0).TOP-REAL n by RLVECT_3:29;
end;
assume v in (0).TOP-REAL n;
then v = 0.TOP-REAL n by RLVECT_3:29;
hence v in Lin(A) /\ Lin(A2) by RLSUB_1:17;
end;
hence thesis by RLSUB_1:31;
end;
then dim TOP-REAL n = dim Lin A + dim Lin A2
by RLVECT_5:37,A13,RLSUB_2:def 4;
then n = dim Lin A + 1 by A11,RLAFFIN3:4;
hence card A = n - 1 by RLVECT_5:29;
thus [#]Lin(A) = Plane(p,0.TOP-REAL n) by A10,RLVECT_5:20;
end;
theorem Th27:
p1<>0.TOP-REAL n & p2<>0.TOP-REAL n implies
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
assume p1<>0.TOP-REAL n; then
consider B1 be linearly-independent Subset of TOP-REAL n such that
A1: card B1 = n - 1 & [#]Lin(B1) = Plane(p1,0.TOP-REAL n) by Th26;
assume p2<>0.TOP-REAL n; then
consider B2 be linearly-independent Subset of TOP-REAL n such that
A2: card B2 = n - 1 & [#]Lin(B2) = Plane(p2,0.TOP-REAL n) by Th26;
consider M be Matrix of n,F_Real such that
A3: M is invertible & (Mx2Tran M).:[#]Lin B1 = [#]Lin B2 by A1,A2,MATRTOP2:22;
reconsider M as invertible Matrix of n,F_Real by A3;
take Mx2Tran M;
thus thesis by A1,A2,A3;
end;
definition
let n;
let p,q;
func TPlane(p,q) -> non empty SubSpace of TOP-REAL n equals
(TOP-REAL n) | Plane(p,q);
correctness
proof
|( p,0.TOP-REAL n )| = 0 by EUCLID_2:32;
then |( p,q-q )| = 0 by RLVECT_1:5;
then q in Plane(p,q);
hence thesis;
end;
end;
theorem Th28:
Base_FinSeq(n+1,n+1) = (0.TOP-REAL n) ^ <* 1 *>
proof
set N = Base_FinSeq(n+1,n+1);
set p = 0.TOP-REAL n;
set q = <* 1 *>;
A1: dom N = Seg (n + 1) by FINSEQ_1:89
.= Seg (n + len q) by FINSEQ_1:39
.= Seg (len p + len q) by CARD_1:def 7;
A2: for k st k in dom p holds N.k = p.k
proof
let k;
assume k in dom p;
then
k in Seg n by FINSEQ_1:89;
then
A3: 1 <= k & k <= n by FINSEQ_1:1;
0+n <= 1+n by XREAL_1:6;
then
A4: k <= n+1 by A3,XXREAL_0:2;
A5: n+1 <> k by A3,NAT_1:13;
thus N.k = 0 by A4,A3,A5,MATRIXR2:76
.= (0*n).k
.= p.k by EUCLID:70;
end;
for k st k in dom q holds N.(len p + k) = q.k
proof
let k;
assume k in dom q;
then k in {1} by FINSEQ_1:2,38;
then A6: k = 1 by TARSKI:def 1;
A7: 0+1 <= n+1 by XREAL_1:6;
thus N.(len p + k) = Base_FinSeq(n+1,n+1).(n+1) by A6,CARD_1:def 7
.= 1 by A7,MATRIXR2:75
.= q.k by A6;
end;
hence thesis by A1,A2,FINSEQ_1:def 7;
end;
Lm3: 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
let p0 be Point of TOP-REAL(n+1) such that
A1: p0 = Base_FinSeq(n+1,n+1);
set T = TOP-REAL n;
set S = TPlane(p0, 0.TOP-REAL(n+1));
defpred P[set, set] means
for p being Element of T st $1=p holds $2 = p^<* 0 *>;
A2: for p being Element of T holds p^<* 0 *> is Element of S
proof
let p be Element of T;
A3: len p = n by CARD_1:def 7;
A4: len(p^<* 0 *>) = n+1 by CARD_1:def 7;
rng(p^<* 0 *>) c= REAL;
then p^<* 0 *> in REAL(n+1) by A4,FINSEQ_2:132;
then reconsider q = p^<* 0 *> as Point of TOP-REAL(n+1) by EUCLID:22;
reconsider r0 = 0 as Real;
dom p0 = Seg(n+1) & dom q = Seg(n+1) by FINSEQ_1:89;
then dom p0 /\ dom q = Seg(n+1);
then
A5: dom mlt(p0,q) = Seg(n+1) by VALUED_1:def 4;
for y being object holds y in rng mlt(p0,q) iff y = r0
proof
let y be object;
set f = mlt(p0,q);
A6: now
let x be set;
assume x in Seg(n+1);
then consider k be Nat such that
A7: x = k & 1 <= k & k <= n+1;
A8: f.x = (p0.x) * (q.x) by VALUED_1:5;
per cases;
suppose
A9: k = n+1;
1 <= len <* r0 *> by FINSEQ_1:39;
then q.(len p + 1) = <* r0 *>.1 by FINSEQ_1:65 .= r0;
hence f.x = r0 by A8,A7,A9,A3;
end;
suppose k <> n+1;
then p0.x = 0 by A1,A7,MATRIXR2:76;
hence f.x = r0 by A8;
end;
end;
hereby
assume y in rng f;
then consider x be object such that
A10: x in dom f & y = f.x by FUNCT_1:def 3;
thus y = r0 by A10,A5,A6;
end;
assume
A11: y = r0;
consider x be object such that
A12: x in Seg(n+1) by XBOOLE_0:def 1;
y = f.x by A11,A12,A6;
hence y in rng f by A12,A5,FUNCT_1:def 3;
end;
then mlt(p0,q) = Seg(n+1) --> r0 by A5,FUNCOP_1:9,TARSKI:def 1;
then
A14: mlt(p0,q) = (n+1) |-> r0 by FINSEQ_2:def 2;
A15: |( p0,q )| = Sum mlt(p0,q)
by RVSUM_1:def 16 .= (n+1)*r0 by A14,RVSUM_1:80 .= 0;
|( p0,q - 0.TOP-REAL(n+1) )| = |( p0,q )| - |( p0,0.TOP-REAL(n+1) )|
by EUCLID_2:27
.= |( p0,q )| - 0 by EUCLID_2:32 .= 0 by A15;
then p^<* 0 *> in Plane(p0, 0.TOP-REAL(n+1));
then p^<* 0 *> in [#]S by PRE_TOPC:def 5;
hence p^<* 0 *> is Element of S;
end;
A16: for x being Element of T ex y being Element of S st P[x,y]
proof
let x be Element of T;
set y = x^<* 0 *>;
reconsider y as Element of S by A2;
take y;
thus P[x,y];
end;
consider f be Function of T,S such that
A17: for x being Element of T holds P[x,f.x] from FUNCT_2:sch 3(A16);
A18: dom f = [#]T by FUNCT_2:def 1;
A19: for y being object holds y in [#]S iff
ex x being object st x in dom f & y = f.x
proof
let y be object;
hereby
assume y in [#]S;
then y in Plane(p0, 0.TOP-REAL(n+1)) by PRE_TOPC:def 5;
then consider q be Point of TOP-REAL(n+1) such that
A20: y = q & |( p0, q - 0.TOP-REAL(n+1) )| = 0;
A21: len q = n+1 & rng q c= REAL by CARD_1:def 7;
then reconsider q1 = q as FinSequence of REAL by FINSEQ_1:def 4;
set p = q1 | n;
reconsider x = p as object;
take x;
0+n <= 1+n by XREAL_1:6;
then
A22: len p = n by A21,FINSEQ_1:59;
A23: rng p c= REAL;
A24: p in REAL n by A22,A23,FINSEQ_2:132;
hence x in dom f by A18,EUCLID:22;
reconsider x1 = x as Element of T by A24,EUCLID:22;
P[x1,f.x1] by A17;
then
A25: f.x = p^<* 0 *>;
A26: q = p ^ <* q.(n+1) *> by CARD_1:def 7,FINSEQ_3:55;
A27: |( p0,q - 0.TOP-REAL(n+1) )| = |( p0,q )| - |( p0,0.TOP-REAL(n+1) )|
by EUCLID_2:27 .= |( p0,q )| - 0 by EUCLID_2:32 .= |( p0,q )|;
reconsider f0 = 0.TOP-REAL n as FinSequence of REAL by EUCLID:24;
rng <* 1 *> c= REAL;
then reconsider f1 = <* 1 *> as FinSequence of REAL by FINSEQ_1:def 4;
reconsider f3 = <* q.(n+1) *> as FinSequence of REAL by RVSUM_1:145;
p in REAL n by A22,A23,FINSEQ_2:132;
then reconsider p1 = p as Point of TOP-REAL n by EUCLID:22;
A28: |( f0 ^ f1, p ^ f3 )| = 0 by A1,A26,A27,A20,Th28;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
0.TOP-REAL n in the carrier of TOP-REAL n;
then f0 in REAL n by EUCLID:22;
then f0 in Funcs(Seg n1,REAL) by FINSEQ_2:93;
then consider g be Function such that
A29: f0 = g & dom g = Seg n1 & rng g c= REAL by FUNCT_2:def 2;
A30: len f0 = len p by A22,A29,FINSEQ_1:def 3;
len f1 = 1 by FINSEQ_1:39 .= len f3 by FINSEQ_1:39;
then |( 0.TOP-REAL n, p1 )| + |( f1, f3 )| = 0 by A28,A30,Th15;
then 0 + |( f1, f3 )| = 0 by EUCLID_2:33;
then Sum mlt(f1,f3) = 0 by RVSUM_1:def 16;
then Sum <* 1*q.(n+1) *> = 0 by RVSUM_1:62;
hence y = f.x by A20,A25,A26,RVSUM_1:73;
end;
given x be object such that
A31: x in dom f & y = f.x;
reconsider p = x as Element of T by A31;
P[p,f.p] by A17;
hence y in [#]S by A31;
end;
then
A32: rng f = [#]S by FUNCT_1:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A33: x1 in dom f & x2 in dom f;
assume
A34: f.x1 = f.x2;
reconsider p1=x1, p2=x2 as Element of T by A33;
f.p1 = p1^<* 0 *> & f.p2 = p2^<* 0 *> by A17;
hence x1 = x2 by A34,FINSEQ_1:33;
end;
then
A35: f is one-to-one;
set T1 = TOP-REAL(n+1);
A36: for p1 being Point of T holds f.p1 is Point of T1
proof
let p1 be Point of T;
[#]S c= [#]T1 by PRE_TOPC:def 4;
hence f.p1 is Point of T1;
end;
A37: for p1 being Point of T, q1 being Point of T1
st q1 = f.p1 holds |. p1 .| = |. q1 .|
proof
let p1 be Point of T;
let q1 be Point of T1;
assume q1 = f.p1;
then
A38: q1 = p1^<* 0 *> by A17;
reconsider x = q1 as Element of REAL(n+1) by EUCLID:22;
A39: len p1 = n & rng p1 c= REAL by CARD_1:def 7;
A40: x|n = (p1^<* 0 *>) | (dom p1) by A38,FINSEQ_1:89
.= p1 by FINSEQ_1:21;
A41: x.(n+1) = 0 by A38,A39,FINSEQ_1:42;
A42: |. q1 .|^2 = |. p1 .|^2 + 0^2 by A40,A41,REAL_NS1:10
.= |. p1 .|^2 + 0 * 0 by SQUARE_1:def 1 .= |. p1 .|^2;
|. q1 .|*|. q1 .| >= 0;
then
A43: |. q1 .|^2 >= 0 by SQUARE_1:def 1;
|. p1 .|*|. p1 .| >= 0;
then |. p1 .|^2 >= 0 by SQUARE_1:def 1;
hence |. p1 .| = sqrt(|. q1 .|^2) by A42,SQUARE_1:def 2
.= |. q1 .| by A43,SQUARE_1:def 2;
end;
A44: for p1,p2 being Point of T, q1,q2 being Point of T1
st q1 = f.p1 & q2 = f.p2 holds f.(p1-p2) = q1 - q2
proof
let p1,p2 be Point of T;
let q1,q2 be Point of T1;
assume q1 = f.p1;
then
A45: q1 = p1^<* 0 *> by A17;
assume q2 = f.p2;
then
A46: q2 = p2^<* 0 *> by A17;
A47: f.(p1-p2) = (p1-p2)^<* 0 *> by A17;
reconsider qa = f.(p1-p2) as Point of T1 by A36;
A48: dom((p1-p2)^<* 0 *>) = Seg(n+1) by FINSEQ_1:89
.= dom(q1-q2) by FINSEQ_1:89;
for k being Nat st k in dom(q1-q2)
holds (q1-q2).k = ((p1-p2)^<* 0 *>).k
proof
let k be Nat;
assume k in dom(q1 - q2);
then
A49: k in Seg(n+1) by FINSEQ_1:89;
A50: (q1-q2).k
= q1.k + (-q2).k by A49,Th16 .= q1.k + ((-1)*q2).k by RLVECT_1:16
.= q1.k + (-1)*(q2.k) by VALUED_1:6;
A51: k in (Seg n \/ {n+1}) by A49,FINSEQ_1:9;
per cases by A51,XBOOLE_0:def 3;
suppose
A52: k in Seg n;
then k in dom p1 & k in dom p2 by FINSEQ_1:89;
then
A53: q1.k = p1.k & q2.k = p2.k by A45,A46,FINSEQ_1:def 7;
k in dom(p1-p2) by A52,FINSEQ_1:89;
then ((p1-p2)^<* 0 *>).k = (p1-p2).k by FINSEQ_1:def 7
.= p1.k + (-p2).k by A52,Th16
.= p1.k + ((-1)*p2).k by RLVECT_1:16 .= p1.k + (-1)*(p2.k) by
VALUED_1:6;
hence thesis by A50,A53;
end;
suppose k in {n+1};
then
A54: k = n + 1 by TARSKI:def 1;
len p1 = n & len p2 = n by CARD_1:def 7;
then
A55: q1.k = 0 & q2.k = 0 by A45,A46,A54,FINSEQ_1:42;
len(p1-p2) = n by CARD_1:def 7;
hence thesis by A50,A55,A54,FINSEQ_1:42;
end;
end;
hence f.(p1-p2) = q1 - q2 by A47,A48,FINSEQ_1:13;
end;
A56: f.:[#]T = [#]S by A32,RELSET_1:22;
for P being Subset of T holds P is closed iff f.:P is closed
proof
let P be Subset of T;
hereby
assume P is closed;
then
A57: [#]T \ P in the topology of T by PRE_TOPC:def 2,def 3;
set FQ = {Ball(q,r) where q is Point of T1, r is Real :
ex p being Point of T st q = f.p & Ball(p,r) c= [#]T \ P};
for x being object st x in FQ holds x in bool [#]T1
proof
let x be object;
assume x in FQ;
then consider q be Point of T1, r be Real such that
A58: x = Ball(q,r) &
ex p being Point of T st q = f.p & Ball(p,r) c= [#]T \ P;
thus x in bool [#]T1 by A58;
end;
then reconsider FQ as Subset-Family of T1 by TARSKI:def 3;
B60: for Q being Subset of T1 st Q in FQ holds Q is open
proof
let Q be Subset of T1;
assume Q in FQ;
then consider q be Point of T1, r be Real such that
A59: Q = Ball(q,r) &
ex p being Point of T st q = f.p & Ball(p,r) c= [#]T \ P;
thus Q is open by A59;
end;
set Q = union FQ;
Q is open by B60,TOPS_2:def 1,TOPS_2:19;
then
A61: Q in the topology of T1 by PRE_TOPC:def 2;
for y being Element of S holds y in f.:([#]T \ P) iff y in Q /\ [#]S
proof
let y be Element of S;
hereby
assume y in f.:([#]T \ P);
then consider x be object such that
A62: x in dom f & x in [#]T \ P & y = f.x by FUNCT_1:def 6;
reconsider p = x as Point of T by A62;
reconsider q = y as Point of T1 by A62,A36;
consider r be Real such that
A63: r > 0 & Ball(p,r) c= [#]T \ P by A62,A57,Th24;
A64: Ball(q,r) in FQ by A62,A63;
q in Ball(q,r) by A63,JORDAN:16;
then y in Q by A64,TARSKI:def 4;
hence y in Q /\ [#]S by XBOOLE_0:def 4;
end;
assume y in Q /\ [#]S;
then y in Q by XBOOLE_0:def 4;
then consider Y be set such that
A65: y in Y & Y in FQ by TARSKI:def 4;
consider q be Point of T1, r be Real such that
A66: Y = Ball(q,r) and
A67: ex p being Point of T st q = f.p & Ball(p,r) c= [#]T \ P by A65;
consider p be Point of T such that
A68: q = f.p & Ball(p,r) c= [#]T \ P by A67;
consider x be object such that
A69: x in dom f & y = f.x by A19;
reconsider p1 = x as Point of T by A69;
reconsider q1 = y as Point of T1 by A69,A36;
q1 in {qy where qy is Point of T1 : |. qy - q .| < r}
by A65,A66,TOPREAL9:def 1;
then consider qy be Point of T1 such that
A70: qy = q1 & |. qy - q .| < r;
f.(p1 - p) = q1 - q by A69,A68,A44;
then |. p1 - p .| < r by A70,A37;
then p1 in {px where px is Point of T : |. px - p .| < r};
then p1 in Ball(p,r) by TOPREAL9:def 1;
hence y in f.:([#]T \ P) by A69,A68,FUNCT_1:def 6;
end;
then
A71: f.:([#]T \ P) = Q /\ [#]S by SUBSET_1:3;
[#]S \ f.:P = Q /\ [#]S by A71,A35,A56,FUNCT_1:64;
then [#]S \ f.:P in the topology of S by A61,PRE_TOPC:def 4;
hence f.:P is closed by PRE_TOPC:def 2,def 3;
end;
assume f.:P is closed;
then [#]S \ f.:P in the topology of S by PRE_TOPC:def 3,def 2;
then consider Q be Subset of T1 such that
A72: Q in the topology of T1 & [#]S \ f.:P = Q /\ [#]S by PRE_TOPC:def 4;
for p being Point of T st p in [#]T \ P holds
ex r being Real st r > 0 & Ball(p,r) c= [#]T \ P
proof
let p be Point of T;
assume p in [#]T \ P;
then f.p in f.:([#]T \ P) by A18,FUNCT_1:def 6;
then
A73: f.p in [#]S \ f.:P by A56,A35,FUNCT_1:64;
reconsider q = f.p as Point of T1 by A36;
q in Q by A72,A73,XBOOLE_0:def 4; then
consider r be Real such that
A74: r > 0 & Ball(q,r) c= Q by A72,Th24;
take r;
thus r > 0 by A74;
let x be object;
assume x in Ball(p,r);
then x in {px where px is Point of T : |. px - p .| < r}
by TOPREAL9:def 1;
then consider p1 be Point of T such that
A75: x = p1 & |. p1 - p .| < r;
reconsider q1 = f.p1 as Point of T1 by A36;
f.(p1 - p) = q1 - q by A44;
then |. q1 - q .| < r by A75,A37;
then q1 in {qx where qx is Point of T1 : |. qx - q .| < r};
then q1 in Ball(q,r) by TOPREAL9:def 1;
then q1 in Q /\ [#]S by A74,XBOOLE_0:def 4;
then not q1 in f.:P by A72,XBOOLE_0:def 5;
then not x in P by A18,A75,FUNCT_1:def 6;
hence x in [#]T \ P by A75,XBOOLE_0:def 5;
end;
then [#]T \ P is open by Th24,PRE_TOPC:def 2;
hence P is closed by PRE_TOPC:def 3;
end;
hence thesis by T_0TOPSP:def 1,A18,A32,A35,TOPS_2:58;
end;
theorem Th29:
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
set T1 = TOP-REAL(n+1);
let p,q be Point of T1;
assume
A1: p <> 0.T1;
reconsider p0 = Base_FinSeq(n+1,n+1) as Point of T1 by EUCLID:22;
A2: p0 <> 0.T1
proof
assume
A3: p0 = 0.T1;
0+1 <= n+1 by XREAL_1:6;
then |. p0 .| = 1 by EUCLID_7:28;
hence contradiction by A3,EUCLID_2:39;
end;
A4: TOP-REAL n, TPlane(p0, 0.TOP-REAL(n+1)) are_homeomorphic by Lm3;
ex R being Function of T1,T1 st R is being_homeomorphism &
R .: Plane(p0,0.T1) = Plane(p,0.T1) by A1,A2,Th27;
then TPlane(p0, 0.T1), TPlane(p,0.T1) are_homeomorphic
by METRIZTS:3,def 1;
then
A5: TOP-REAL n, TPlane(p,0.T1) are_homeomorphic by A4,BORSUK_3:3;
transl(q,T1) .: Plane(p,0.T1) = Plane(p,0.T1+q) by Th25
.= Plane(p,q) by RLVECT_1:4;
then T1|Plane(p, 0.T1), T1|Plane(p,q) are_homeomorphic by METRIZTS:3,def 1;
hence thesis by A5,BORSUK_3:3;
end;
theorem
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
let p,q be Point of TOP-REAL(n+1);
assume p <> 0.TOP-REAL(n+1);
then TOP-REAL n, TPlane(p,q) are_homeomorphic by Th29;
hence thesis by Th12;
end;
begin :: Spheres
definition
let n;
func TUnitSphere(n) -> TopSpace equals
Tunit_circle(n+1);
correctness;
end;
registration
let n;
cluster TUnitSphere(n) -> non empty;
correctness;
end;
:: stereographic projection
definition
let n,p;
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:
for q st q in S holds it.q = 1/(1-|(q,p)|)*(q - |(q,p)|*p);
existence
proof
set T = TPlane(p,0.TOP-REAL n);
defpred P[object,object] means
for q being Point of TOP-REAL n st q=$1 & q in S
holds $2 = 1/(1-|(q,p)|)*(q - |(q,p)|*p);
A2: for x being object st x in [#]S ex y being object st y in [#]T & P[x,y]
proof
let x be object;
assume
A3: x in [#]S;
[#]S c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider q=x as Point of TOP-REAL n by A3;
set y = 1/(1-|(q,p)|)*(q - |(q,p)|*p);
take y;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
reconsider p1=p as Point of TOP-REAL n1;
|.p1 - 0.TOP-REAL n1.| = 1 by A1,TOPREAL9:9;
then |.p1 + (-1)*0.TOP-REAL n1.| = 1 by RLVECT_1:16;
then |.p1 + 0.TOP-REAL n1.| = 1 by RLVECT_1:10;
then |. p .| = 1 by RLVECT_1:4;
then |( p, p)| = 1^2 by EUCLID_2:4;
then
A4: |(p, p)| = 1*1 by SQUARE_1:def 1;
A5: |(p, |(q,p)|*p)| = |(q,p)|*|(p, p)| by EUCLID_2:20 .= |(p,q)| by A4;
|(p,y)| = 1/(1-|(q,p)|)*|(p, q - |(q,p)|*p)| by EUCLID_2:20
.= 1/(1-|(q,p)|)*(|(p, q)| - |(p, |(q,p)|*p)|) by EUCLID_2:27
.= 0 by A5;
then |(p,y + 0.TOP-REAL n)|=0 by RLVECT_1:4;
then |(p,y + (-1)*0.TOP-REAL n)|=0 by RLVECT_1:10;
then |(p,y - 0.TOP-REAL n)|=0 by RLVECT_1:16;
then y in Plane(p,0.TOP-REAL n);
hence y in [#]T by PRE_TOPC:def 5;
thus P[x,y];
end;
consider f be Function of [#]S, [#]T such that
A6: for x being object st x in [#]S holds P[x,f.x] from FUNCT_2:sch 1(A2);
reconsider f as Function of S, T;
take f;
let q be Point of TOP-REAL n;
assume
A7: q in S;
thus thesis by A6,A7;
end;
uniqueness
proof
let f1, f2 be Function of S,TPlane(p,0.TOP-REAL n) such that
A8: for q being Point of TOP-REAL n st q in S holds
f1.q = 1/(1-|(q,p)|)*(q - |(q,p)|*p) and
A9: for q being Point of TOP-REAL n st q in S holds
f2.q = 1/(1-|(q,p)|)*(q - |(q,p)|*p);
for x being object st x in [#]S holds f1.x = f2.x
proof
let x be object;
assume
A10: x in [#]S;
[#]S c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider q = x as Point of TOP-REAL n by A10;
A11: q in S by A10;
thus f1.x = 1/(1-|(q,p)|)*(q - |(q,p)|*p) by A11,A8 .= f2.x by A11,A9;
end;
hence f1=f2 by FUNCT_2:12;
end;
end;
theorem Th31:
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
let S be SubSpace of TOP-REAL n;
assume
A1: [#]S = Sphere(0.TOP-REAL n,1) \ {p};
assume
A2: p in Sphere(0.TOP-REAL n,1);
set f = stereographic_projection(S,p);
set T = TPlane(p,0.TOP-REAL n);
A3: dom f = [#]S by FUNCT_2:def 1;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
reconsider p1=p as Point of TOP-REAL n1;
|.p1 - 0.TOP-REAL n1.| = 1 by A2,TOPREAL9:9;
then |.p1 + (-1)*0.TOP-REAL n1.| = 1 by RLVECT_1:16;
then |.p1 + 0.TOP-REAL n1.| = 1 by RLVECT_1:10;
then
A4: |. p .| = 1 by RLVECT_1:4;
then |( p,p)| = 1^2 by EUCLID_2:4;
then
A5: |( p,p)| = 1*1 by SQUARE_1:def 1;
defpred P[object,object] means
for q being Point of TOP-REAL n st q=$1 & q in T
holds $2 = 1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p);
A6: for x being object st x in [#]T ex y being object st y in [#]S & P[x,y]
proof
let x be object;
assume
A7: x in [#]T;
[#]T c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider q=x as Point of TOP-REAL n by A7;
set y = 1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p);
take y;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
reconsider p1=p as Point of TOP-REAL n1;
q in Plane(p,0.TOP-REAL n) by A7,PRE_TOPC:def 5;
then consider x1 be Point of TOP-REAL n such that
A8: x1=q & |(p,x1 - 0.TOP-REAL n)| = 0;
|(p,q + (-1)*0.TOP-REAL n)|=0 by A8,RLVECT_1:16;
then |(p,q + 0.TOP-REAL n)|=0 by RLVECT_1:10;
then
A9: |(p,q)|=0 by RLVECT_1:4;
A10: |(q,q)| >= 0 by EUCLID_2:35;
A11: not y in {p}
proof
assume
A12: y in {p};
A13: |(2*q +(|(q,q)|-1)*p, p)|
= 2*|(q,p)| + (|(q,q)|-1)*|(p,p)| by EUCLID_2:25
.= (|(q,q)|-1)*|(p,p)| by A9;
|(1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p),p)|
= (1/(|(q,q)|+1))*|( 2*q +(|(q,q)|-1)*p,p)| by EUCLID_2:19
.= (1/(|(q,q)|+1))*(|(q,q)|-1)*|(p,p)| by A13;
then (|(q,q)|+1)*1 = (|(q,q)|+1)*((1/(|(q,q)|+1))*(|(q,q)|-1))
by A5,A12,TARSKI:def 1
.= (|(q,q)|+1)*(1/(|(q,q)|+1))*(|(q,q)|-1)
.= (|(q,q)|+1)/(|(q,q)|+1)*(|(q,q)|-1) by XCMPLX_1:99
.= 1*(|(q,q)|-1) by A10,XCMPLX_1:60;
hence contradiction;
end;
reconsider y1=y as Point of TOP-REAL n1;
A14: |( q ,2*q +(|(q,q)|-1)*p )|
= 2*|( q, q )| + (|(q,q)|-1)*|( p, q )| by EUCLID_2:25
.= 2*|( q, q )| by A9;
A15: |( p,2*q +(|(q,q)|-1)*p )|
= 2*|( q, p )| + (|(q,q)|-1)*|( p, p )| by EUCLID_2:25
.= (|(q,q)|-1) by A5,A9;
A16: |( 2*q +(|(q,q)|-1)*p,2*q +(|(q,q)|-1)*p )|
= 2*(2*|(q,q)|) + (|(q,q)|-1)*|( p,2*q +(|(q,q)|-1)*p )| by A14,EUCLID_2:25
.= (|(q,q)|+1)*(|(q,q)|+1) by A15;
A17: |( 2*q +(|(q,q)|-1)*p,1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p) )|
= 1/(|(q,q)|+1)*|( 2*q +(|(q,q)|-1)*p,2*q +(|(q,q)|-1)*p )|
by EUCLID_2:20;
|( 1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p),1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p) )|
=1/(|(q,q)|+1)*|( 2*q +(|(q,q)|-1)*p,1/(|(q,q)|+1)*(2*q +(|(q,q)|-1)*p) )|
by EUCLID_2:19
.= 1/(|(q,q)|+1)*(1/(|(q,q)|+1)*(|(q,q)|+1))*(|(q,q)|+1) by A16,A17
.= 1/(|(q,q)|+1)*((|(q,q)|+1)/(|(q,q)|+1))*(|(q,q)|+1) by XCMPLX_1:99
.= 1/(|(q,q)|+1)*1*(|(q,q)|+1) by A10,XCMPLX_1:60
.= (|(q,q)|+1)/(|(q,q)|+1) by XCMPLX_1:99
.= 1 by A10,XCMPLX_1:60;
then |. y .| = 1 by EUCLID_2:5,SQUARE_1:18;
then |.y + 0.TOP-REAL n.| = 1 by RLVECT_1:4;
then |.y + (-1)*0.TOP-REAL n.| = 1 by RLVECT_1:10;
then |.y - 0.TOP-REAL n.| = 1 by RLVECT_1:16;
then y1 in Sphere(0.TOP-REAL n,1) by TOPREAL9:9;
hence y in [#]S by A1,A11,XBOOLE_0:def 5;
thus P[x,y];
end;
consider g1 be Function of [#]T, [#]S such that
A18: for x being object st x in [#]T holds P[x,g1.x] from FUNCT_2:sch 1(A6);
reconsider g = g1 as Function of T, S;
reconsider f1 = f as Function of [#]S, [#]T;
|. 0.TOP-REAL n .| <> |. p .| by A4,EUCLID_2:39;
then 0.TOP-REAL n <> (1+1)*p by RLVECT_1:11;
then 0.TOP-REAL n <> 1*p + 1*p by RLVECT_1:def 6;
then 0.TOP-REAL n <> 1*p + p by RLVECT_1:def 8;
then 0.TOP-REAL n <> p + p by RLVECT_1:def 8;
then p + -p <> p + p by RLVECT_1:5;
then
A19: not -p in {p} by TARSKI:def 1;
|. -p .| = 1 by A4,EUCLID:71;
then |.-p + 0.TOP-REAL n.| = 1 by RLVECT_1:4;
then |.-p + (-1)*0.TOP-REAL n.| = 1 by RLVECT_1:10;
then |.-p - 0.TOP-REAL n.| = 1 by RLVECT_1:16;
then
A20: -p in Sphere(0.TOP-REAL n1,1) by TOPREAL9:9;
then
A21: [#]S <> {} by A1,A19,XBOOLE_0:def 5;
A22: for y,x being object holds y in [#]T & g1.y = x iff x in [#]S & f1.x = y
proof
let y,x be object;
hereby
assume
A23: y in [#]T;
assume
A24: g1.y = x;
hence
A25: x in [#]S by A23,A21,FUNCT_2:5;
[#]S c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider qx = x as Point of TOP-REAL n by A25;
[#]T c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider qy = y as Point of TOP-REAL n by A23;
qy in T by A23;
then
A26: qx = 1/(|(qy,qy)|+1)*(2*qy +(|(qy,qy)|-1)*p) by A18,A24;
qx in S by A24,A23,A21,FUNCT_2:5;
then
A27: f.qx = 1/(1-|(qx,p)|)*(qx - |(qx,p)|*p) by A2,Def5;
qy in Plane(p,0.TOP-REAL n) by A23,PRE_TOPC:def 5;
then consider y1 be Point of TOP-REAL n such that
A28: y1=qy & |(p,y1 - 0.TOP-REAL n)| = 0;
|(p,qy + (-1)*0.TOP-REAL n)|=0 by A28,RLVECT_1:16;
then |(p,qy + 0.TOP-REAL n)|=0 by RLVECT_1:10;
then
A29: |(p,qy)|=0 by RLVECT_1:4;
A30: |( 2*qy +(|(qy,qy)|-1)*p, p)|
= 2*|(qy,p)| + (|(qy,qy)|-1)*|(p,p)| by EUCLID_2:25
.= |(qy,qy)| -1 by A5,A29;
A31: |(qx,p)|
= 1/(|(qy,qy)|+1)*|( 2*qy +(|(qy,qy)|-1)*p, p)| by A26,EUCLID_2:19
.= (|(qy,qy)|-1)/(|(qy,qy)|+1)*1 by A30,XCMPLX_1:75;
A32: |(qy,qy)| >= 0 by EUCLID_2:35;
A33: 1-|(qx,p)| = (|(qy,qy)|+1)/(|(qy,qy)|+1) - (|(qy,qy)|-1)/(|(qy,qy)|+1)
by A31,A32,XCMPLX_1:60
.= ((|(qy,qy)|+1) - (|(qy,qy)|-1))/(|(qy,qy)|+1) by XCMPLX_1:120
.= 2/(|(qy,qy)|+1);
A34: 1/(1-|(qx,p)|) = (|(qy,qy)|+1)/2 by A33,XCMPLX_1:57;
A35: ((|(qy,qy)|+1)/2)*qx
= (((|(qy,qy)|+1)/2)*(1/(|(qy,qy)|+1)))*(2*qy +(|(qy,qy)|-1)*p)
by A26,RLVECT_1:def 7
.= (((|(qy,qy)|+1)*1)/(2*(|(qy,qy)|+1)))*(2*qy +(|(qy,qy)|-1)*p)
by XCMPLX_1:76
.= (((|(qy,qy)|+1)/(|(qy,qy)|+1))*(1/2))*(2*qy +(|(qy,qy)|-1)*p)
by XCMPLX_1:76
.= (1*(1/2))*(2*qy +(|(qy,qy)|-1)*p) by A32,XCMPLX_1:60
.= (1/2)*(2*qy) +(1/2)*((|(qy,qy)|-1)*p) by RLVECT_1:def 5
.= ((1/2)*2)*qy +(1/2)*((|(qy,qy)|-1)*p) by RLVECT_1:def 7
.= (1)*qy +(1/2*(|(qy,qy)|-1))*p by RLVECT_1:def 7
.= qy +((|(qy,qy)|-1)/2)*p by RLVECT_1:def 8;
A36: ((|(qy,qy)|+1)/2)*|(qx,p)|
= ((|(qy,qy)|+1)/(|(qy,qy)|+1))*((|(qy,qy)|-1)/2) by A31,XCMPLX_1:85
.= 1*((|(qy,qy)|-1)/2) by A32,XCMPLX_1:60
.= (|(qy,qy)|-1)/2;
thus f1.x = ((|(qy,qy)|+1)/2)*qx-((|(qy,qy)|+1)/2)*(|(qx,p)|*p)
by A27,A34,RLVECT_1:34
.= ((|(qy,qy)|+1)/2)*qx - ((|(qy,qy)|-1)/2)*p by A36,RLVECT_1:def 7
.= y by A35,RLVECT_4:1;
end;
assume
A37: x in [#]S;
assume
A38: f1.x = y;
hence y in [#]T by A37,FUNCT_2:5;
[#]S c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider qx = x as Point of TOP-REAL n by A37;
qx in S by A37;
then
A40: y = 1/(1-|(qx,p)|)*(qx - |(qx,p)|*p) by A38,A2,Def5;
then reconsider qy = y as Point of TOP-REAL n;
A41: qy in T by A38,A37,FUNCT_2:5;
A42: g1.qy = 1/(|(qy,qy)|+1)*(2*qy +(|(qy,qy)|-1)*p) by A41,A18;
reconsider qx1 = qx as Point of TOP-REAL n1;
qx1 in Sphere(0.TOP-REAL n,1) by A37,A1,XBOOLE_0:def 5;
then |.qx1 - 0.TOP-REAL n1.| = 1 by TOPREAL9:9;
then |.qx1 + (-1)*0.TOP-REAL n1.| = 1 by RLVECT_1:16;
then |.qx1 + 0.TOP-REAL n1.| = 1 by RLVECT_1:10;
then |. qx .| = 1 by RLVECT_1:4;
then |( qx,qx)| = 1^2 by EUCLID_2:4;
then
A43: |( qx,qx)| = 1*1 by SQUARE_1:def 1;
A44: |( |(qx,p)|*p, qx-|(qx,p)|*p )|
= |( |(qx,p)|*p, qx )| - |( |(qx,p)|*p, |(qx,p)|*p )| by EUCLID_2:27
.= |(qx,p)|*|(qx,p)| - |( |(qx,p)|*p, |(qx,p)|*p )| by EUCLID_2:19
.= |(qx,p)|*|(qx,p)| - |(qx,p)|*|( p, |(qx,p)|*p )| by EUCLID_2:19
.= |(qx,p)|*|(qx,p)| - |(qx,p)|*(|(qx,p)|*|( p,p )|) by EUCLID_2:20
.= 0 by A5;
A45: |( qx, qx-|(qx,p)|*p )| = |(qx,qx)| - |(qx,|(qx,p)|*p )| by EUCLID_2:24
.= 1 - |(qx,p)|*|(qx,p)| by A43,EUCLID_2:20;
A46: |( qx-|(qx,p)|*p, qx-|(qx,p)|*p )|
= |( qx, qx-|(qx,p)|*p )| - |( |(qx,p)|*p, qx-|(qx,p)|*p )| by EUCLID_2:24
.= 1 - |(qx,p)|*|(qx,p)| + 0 by A45,A44;
|(qx,p)| <> 1
proof
assume
A47: |(qx,p)| = 1;
A48: not qx in {p} by A1,A37,XBOOLE_0:def 5;
|(qx,p)| - |( qx,qx)| = 0 by A43,A47;
then
A49: |(qx,p - qx)| = 0 by EUCLID_2:27;
|( p,p)| - |(qx,p)| = 0 by A5,A47;
then
A50: |(p - qx,p)| = 0 by EUCLID_2:24;
|(p - qx, p - qx)| = 0 - 0 by A49,A50,EUCLID_2:24;
then p - qx = 0.TOP-REAL n by EUCLID_2:41;
then p = qx by RLVECT_1:21;
hence contradiction by A48,TARSKI:def 1;
end;
then
A51: 1-|(qx,p)| <> 0;
then
A52: (1-|(qx,p)|)*(1-|(qx,p)|) <> 0;
A53: |(qy,qy)| = 1/(1-|(qx,p)|) * |( qx-|(qx,p)|*p,qy )| by A40,EUCLID_2:19
.= 1/(1-|(qx,p)|) * (1/(1-|(qx,p)|)*
|( qx-|(qx,p)|*p, qx-|(qx,p)|*p )|) by A40,EUCLID_2:19
.= 1/(1-|(qx,p)|)*(1/(1-|(qx,p)|))*(1 - |(qx,p)|*|(qx,p)|) by A46
.= 1/((1-|(qx,p)|)*(1-|(qx,p)|))*(1 - |(qx,p)|*|(qx,p)|) by XCMPLX_1:102
.= (1-|(qx,p)|*|(qx,p)|)/(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|) by XCMPLX_1:99;
A54: |(qy,qy)|+1 = (1-|(qx,p)|*|(qx,p)|)/(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|) +
(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)/(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)
by A53,A52,XCMPLX_1:60
.= ((1-|(qx,p)|*|(qx,p)|)+(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)) /
(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|) by XCMPLX_1:62
.= 2*(1-|(qx,p)|)/(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)
.= 2*((1-|(qx,p)|)/((1-|(qx,p)|)*(1-|(qx,p)|))) by XCMPLX_1:74
.= 2*((1-|(qx,p)|)/(1-|(qx,p)|)/(1-|(qx,p)|)) by XCMPLX_1:78
.= 2*(1/(1-|(qx,p)|)) by A51,XCMPLX_1:60
.= (2*1)/(1-|(qx,p)|) by XCMPLX_1:74;
A55: |(qy,qy)|-1 = (1-|(qx,p)|*|(qx,p)|)/(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)-
(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)/(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)
by A53,A52,XCMPLX_1:60
.= ((1-|(qx,p)|*|(qx,p)|)-(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|)) /
(1-2*|(qx,p)|+|(qx,p)|*|(qx,p)|) by XCMPLX_1:120
.= 2*|(qx,p)|*(1-|(qx,p)|)/((1-|(qx,p)|)*(1-|(qx,p)|))
.= 2*|(qx,p)|*((1-|(qx,p)|)/((1-|(qx,p)|)*(1-|(qx,p)|))) by XCMPLX_1:74
.= 2*|(qx,p)|*((1-|(qx,p)|)/(1-|(qx,p)|)/(1-|(qx,p)|)) by XCMPLX_1:78
.= 2*|(qx,p)|*(1/(1-|(qx,p)|)) by A51,XCMPLX_1:60
.= (2*|(qx,p)|*1)/(1-|(qx,p)|) by XCMPLX_1:74;
A56: 1/(|(qy,qy)|+1) = (1-|(qx,p)|)/2 by A54,XCMPLX_1:57;
A57: (|(qy,qy)|-1)/(|(qy,qy)|+1)
= (2*|(qx,p)|)/((1-|(qx,p)|)*(2/(1-|(qx,p)|))) by A54,A55,XCMPLX_1:78
.= (2*|(qx,p)|)/(2*(1-|(qx,p)|)/(1-|(qx,p)|)) by XCMPLX_1:74
.= (2*|(qx,p)|)/(2*((1-|(qx,p)|)/(1-|(qx,p)|))) by XCMPLX_1:74
.= (2*|(qx,p)|)/(2*1) by A51,XCMPLX_1:60
.= |(qx,p)|;
A58: (1-|(qx,p)|)*qy
= ((1-|(qx,p)|)*(1/(1-|(qx,p)|)))*(qx - |(qx,p)|*p) by A40,RLVECT_1:def 7
.= ((1-|(qx,p)|)*1)/(1-|(qx,p)|)*(qx - |(qx,p)|*p) by XCMPLX_1:74
.= 1*(qx - |(qx,p)|*p) by A51,XCMPLX_1:60
.= qx - |(qx,p)|*p by RLVECT_1:def 8;
thus g1.y = 1/(|(qy,qy)|+1)*(2*qy) + 1/(|(qy,qy)|+1)*((|(qy,qy)|-1)*p)
by A42,RLVECT_1:def 5
.= (1/(|(qy,qy)|+1)*2)*qy + 1/(|(qy,qy)|+1)*((|(qy,qy)|-1)*p) by
RLVECT_1:def 7
.= (1/(|(qy,qy)|+1)*2)*qy + (1/(|(qy,qy)|+1)*(|(qy,qy)|-1))*p by
RLVECT_1:def 7
.= (1-|(qx,p)|)*qy + ((1*(|(qy,qy)|-1))/(|(qy,qy)|+1))*p by A56,XCMPLX_1:74
.= qx - (|(qx,p)|*p - |(qx,p)|*p) by A57,A58,RLVECT_1:29
.= qx - 0.TOP-REAL n by RLVECT_1:5
.= qx + (-1)*0.TOP-REAL n by RLVECT_1:16 .= qx + 0.TOP-REAL n by
RLVECT_1:10
.= x by RLVECT_1:4;
end;
for y being object holds y in [#]T iff
ex x being object st x in dom f & y = f.x
proof
let y be object;
hereby
assume
A59: y in [#]T;
reconsider x = g.y as object;
take x;
thus x in dom f by A22,A3,A59;
thus y = f.x by A59,A22;
end;
given x be object such that
A60: x in dom f & y = f.x;
thus y in [#]T by A60,FUNCT_2:5;
end;
then
A61: rng f = [#]T by FUNCT_1:def 3;
A62: f is one-to-one
proof
let x1,x2 be object;
assume
A63: x1 in dom f & x2 in dom f;
assume
A64: f.x1 = f.x2;
g1.(f.x1) = x1 & g1.(f.x2) = x2 by A63,A22;
hence x1 = x2 by A64;
end;
A65: f is continuous
proof
A66: [#]S c= [#]TOP-REAL n by PRE_TOPC:def 4;
set f0 = InnerProduct(p);
consider f1 be Function of TOP-REAL n1, R^1 such that
A67: (for q being Point of TOP-REAL n holds f1.q=1) & f1 is continuous
by JGRAPH_2:20;
consider f2 be Function of TOP-REAL n,R^1 such that
A68: (for q being Point of TOP-REAL n,r1,r2 being Real
st f1.q=r1 & f0.q=r2 holds f2.q=r1-r2) & f2 is continuous
by A67,JGRAPH_2:21;
reconsider f2 as continuous Function of TOP-REAL n,R^1 by A68;
reconsider S1=S as non empty TopSpace by A20,A1,A19,XBOOLE_0:def 5;
set f3 = f2|S1;
A69: for q being Point of TOP-REAL n st q in S1 holds f3.q = 1 - |(q,p)|
proof
let q be Point of TOP-REAL n;
assume B70: q in S1;
A71: [#]S1 c= [#]TOP-REAL n by PRE_TOPC:def 4;
f0.q = |(q,p)| & f1.q = 1 by Def1,A67;
then
A72: f2.q = 1 - |(q,p)| by A68;
thus f3.q = (f2 | (the carrier of S1)).q by A71,TMAP_1:def 3
.= 1 - |(q,p)| by A72,B70,FUNCT_1:49;
end;
A73: for q being Point of S1 holds f3.q <> 0
proof
let q be Point of S1;
reconsider qx = q as Point of TOP-REAL n by A66;
reconsider qx1 = qx as Point of TOP-REAL n1;
qx1 in Sphere(0.TOP-REAL n,1) by A1,XBOOLE_0:def 5;
then |.qx1 - 0.TOP-REAL n1.| = 1 by TOPREAL9:9;
then |.qx1 + (-1)*0.TOP-REAL n1.| = 1 by RLVECT_1:16;
then |.qx1 + 0.TOP-REAL n1.| = 1 by RLVECT_1:10;
then |. qx .| = 1 by RLVECT_1:4;
then |( qx,qx)| = 1^2 by EUCLID_2:4;
then
A74: |( qx,qx)| = 1*1 by SQUARE_1:def 1;
|(qx,p)| <> 1
proof
assume
A75: |(qx,p)| = 1;
A76: not qx in {p} by A1,XBOOLE_0:def 5;
|(qx,p)| - |( qx,qx)| = 0 by A74,A75;
then
A77: |(qx,p - qx)| = 0 by EUCLID_2:27;
|( p,p)| - |(qx,p)| = 0 by A5,A75;
then
A78: |(p - qx,p)| = 0 by EUCLID_2:24;
|(p - qx, p - qx)| = 0 - 0 by A77,A78,EUCLID_2:24;
then p - qx = 0.TOP-REAL n by EUCLID_2:41;
then p = qx by RLVECT_1:21;
hence contradiction by A76,TARSKI:def 1;
end;
then
A79: 1-|(qx,p)| <> 0;
qx in S1;
hence thesis by A69,A79;
end;
then consider f4 be Function of S1,R^1 such that
A80: (for q being Point of S1,r1 being Real st f3.q=r1
holds f4.q=1/r1) & f4 is continuous by JGRAPH_2:26;
consider f5 be Function of S1,TOP-REAL n1 such that
A81: (for a being Point of S1, b being Point of TOP-REAL n,
r being Real st a = b & f4.a = r holds f5.b = r*b) &
f5 is continuous by A80,MFOLD_1:2;
set f6 = f0|S1;
A82: for q being Point of TOP-REAL n st q in S1 holds f6.q = |(q,p)|
proof
let q be Point of TOP-REAL n;
assume B83:q in S1;
A84: [#]S1 c= [#]TOP-REAL n by PRE_TOPC:def 4;
A85: f0.q = |(q,p)| by Def1;
thus f6.q = (f0 | (the carrier of S1)).q by A84,TMAP_1:def 3
.= |(q,p)| by A85,B83,FUNCT_1:49;
end;
consider f7 be Function of S1,R^1 such that
A86: (for q being Point of S1,r1,r2 being Real
st f6.q=r1 & f3.q=r2 holds f7.q=r1/r2) &
f7 is continuous by A73,JGRAPH_2:27;
reconsider p1 = -p as Point of TOP-REAL n1;
consider f8 be Function of S1,TOP-REAL n1 such that
A87: (for r being Point of S1 holds f8.r=(f7.r)*p1) &
f8 is continuous by A86,JGRAPH_6:9;
consider f9 be Function of S,TOP-REAL n such that
A88: (for r being Point of S1 holds f9.r = f5.r + f8.r) &
f9 is continuous by A87,A81,JGRAPH_6:12;
A89: dom f = [#]S by FUNCT_2:def 1 .= dom f9 by FUNCT_2:def 1;
for x being object st x in dom f holds f.x = f9.x
proof
let x be object;
assume
A90: x in dom f;
then reconsider qx = x as Point of TOP-REAL n by A66;
A91: qx in S by A90;
reconsider r = qx as Point of S1 by A90;
A92: f3.r = 1 - |(qx,p)| by A69,A91;
A93: f4.r = 1/(1 - |(qx,p)|) by A92,A80;
A94: f6.r = |(qx,p)| by A82,A91;
A95: f8.r = (f7.r)*(-p) by A87 .= |(qx,p)|/(1 - |(qx,p)|)*(-p) by A92,A94,A86;
f9.x = f5.r + f8.r by A88
.= (1/(1 - |(qx,p)|))*qx + (1*|(qx,p)|)/(1 - |(qx,p)|)*(-p)
by A93,A81,A95
.= 1/(1-|(qx,p)|)*qx + ((1/(1-|(qx,p)|))*|(qx,p)|)*(-p) by XCMPLX_1:74
.= 1/(1-|(qx,p)|)*qx + (1/(1-|(qx,p)|))*(|(qx,p)|*(-p)) by RLVECT_1:def 7
.= 1/(1-|(qx,p)|)*(qx + |(qx,p)|*(-p)) by RLVECT_1:def 5
.= 1/(1-|(qx,p)|)*(qx - |(qx,p)|*p) by RLVECT_1:25;
hence f.x = f9.x by A91,A2,Def5;
end;
hence thesis by A88,A89,FUNCT_1:2,PRE_TOPC:27;
end;
A96: g is continuous
proof
consider g0 be Function of TOP-REAL n1,R^1 such that
A98: (for q being Point of TOP-REAL n1 holds g0.q = |.q.|)
& g0 is continuous by JORDAN2C:84;
consider g1 be Function of TOP-REAL n,R^1 such that
A99: (for q being Point of TOP-REAL n,r1 being Real st g0.q=r1
holds g1.q=r1*r1) & g1 is continuous by A98,JGRAPH_2:22;
consider g2 be Function of TOP-REAL n,R^1 such that
A100: (for q being Point of TOP-REAL n,r1 being Real st g1.q=r1
holds g2.q=r1+1) & g2 is continuous by A99,JGRAPH_2:24;
consider g3 be Function of TOP-REAL n,R^1 such that
A101: (for q being Point of TOP-REAL n,r1 being Real st g1.q=r1
holds g3.q=r1+(-1)) & g3 is continuous by A99,JGRAPH_2:24;
consider g4 be Function of TOP-REAL n,R^1 such that
A102: (for q being Point of TOP-REAL n holds g4.q=2)
& g4 is continuous by JGRAPH_2:20;
A103: for q being Point of TOP-REAL n holds g2.q<>0
proof
let q be Point of TOP-REAL n;
g0.q = |.q.| by A98;
then g1.q = |.q.|*|.q.| by A99;
then g2.q = |.q.|*|.q.| + 1 by A100;
hence g2.q <> 0;
end;
then consider g5 be Function of TOP-REAL n,R^1 such that
A104: (for q being Point of TOP-REAL n,r1,r2 being Real
st g4.q=r1 & g2.q=r2 holds g5.q=r1/r2) & g5 is continuous
by A102,A100,JGRAPH_2:27;
reconsider g6=g5|T as continuous Function of T, R^1 by A104;
consider g7 be Function of T,TOP-REAL n1 such that
A105: (for a being Point of T,b being Point of TOP-REAL n,
r being Real st a = b & g6.a = r holds g7.b = r*b) &
g7 is continuous by MFOLD_1:2;
consider g8 be Function of TOP-REAL n,R^1 such that
A106: (for q being Point of TOP-REAL n,r1,r2 being Real
st g3.q=r1 & g2.q=r2 holds g8.q=r1/r2) & g8 is continuous
by A103,A100,A101,JGRAPH_2:27;
reconsider p1 = p as Point of TOP-REAL n1;
reconsider g9=g8|T as continuous Function of T, R^1 by A106;
consider g10 be Function of T,TOP-REAL n1 such that
A107: (for r being Point of T holds g10.r=(g9.r)*p1) &
g10 is continuous by JGRAPH_6:9;
consider g11 be Function of T,TOP-REAL n1 such that
A108: (for r being Point of T holds g11.r = g7.r + g10.r) &
g11 is continuous by A105,A107,JGRAPH_6:12;
A109: dom g = [#]T by A21,FUNCT_2:def 1 .= dom g11 by FUNCT_2:def 1;
for x being object st x in dom g holds g.x = g11.x
proof
let x be object;
assume
A110: x in dom g;
[#]T c= [#]TOP-REAL n by PRE_TOPC:def 4;
then reconsider qx = x as Point of TOP-REAL n by A110;
A112: qx in T by A110;
reconsider r = qx as Point of T by A110;
A113: [#]T c= [#]TOP-REAL n by PRE_TOPC:def 4;
A114: g0.qx = |.qx.| by A98;
A115: g1.qx = |.qx.|*|.qx.| by A99,A114 .= |.qx.|^2 by SQUARE_1:def 1
.= |(qx,qx)| by EUCLID_2:4;
A116: g2.qx = |(qx,qx)| + 1 by A100,A115;
A117: g4.qx = 2 by A102;
A118: g6.qx = (g5 | (the carrier of T)).qx by A113,TMAP_1:def 3
.= g5.qx by A110,FUNCT_1:49 .= 2/(|(qx,qx)|+1) by A104,A117,A116;
A119: g3.qx = |(qx,qx)| + (-1) by A101,A115;
A120: g9.qx = (g8 | (the carrier of T)).qx by A113,TMAP_1:def 3
.= g8.qx by A110,FUNCT_1:49
.= (|(qx,qx)| - 1)/(|(qx,qx)| + 1) by A116,A119,A106;
A121: g7.r = 2/(|(qx,qx)|+1) * qx by A105,A118;
g11.x = g7.r + g10.r by A108
.=(1*2)/(|(qx,qx)|+1)*qx + (1*(|(qx,qx)|-1))/(|(qx,qx)|+1)*p
by A120,A107,A121
.=(1*2)/(|(qx,qx)|+1)*qx + 1/(|(qx,qx)|+1)*(|(qx,qx)|-1)*p by XCMPLX_1:74
.= 1/(|(qx,qx)|+1)*2*qx + 1/(|(qx,qx)|+1)*(|(qx,qx)|-1)*p by XCMPLX_1:74
.= 1/(|(qx,qx)|+1)*2*qx + 1/(|(qx,qx)|+1)*((|(qx,qx)|-1)*p) by
RLVECT_1:def 7
.= 1/(|(qx,qx)|+1)*(2*qx)+1/(|(qx,qx)|+1)*((|(qx,qx)|-1)*p) by
RLVECT_1:def 7
.= 1/(|(qx,qx)|+1)*(2*qx +(|(qx,qx)|-1)*p) by RLVECT_1:def 5;
hence g.x = g11.x by A18,A112;
end;
hence thesis by A108,A109,FUNCT_1:2,PRE_TOPC:27;
end;
reconsider f2 = f1 as [#]T-valued Relation;
f2 is onto by A61,FUNCT_2:def 3;
then
A122: f1" = (f1 qua Function)" by A62,TOPS_2:def 4;
g1 = (f1 qua Function)" by A61,A62,A22,A21,FUNCT_2:28;
hence thesis by A3,A61,A62,A65,A96,A122,TOPS_2:def 5;
end;
registration
let n;
cluster TUnitSphere(n) -> second-countable;
correctness;
cluster TUnitSphere(n) -> without_boundary n-locally_euclidean;
correctness
proof
set M = TUnitSphere(n);
for p being Point of M holds
ex U being a_neighborhood of p st U,[#]TOP-REAL n are_homeomorphic
proof
let p be Point of M;
reconsider n1=n+1 as Element of NAT by ORDINAL1:def 12;
[#]Tunit_circle(n+1) c= [#]TOP-REAL(n+1) by PRE_TOPC:def 4;
then reconsider p1 = p as Point of TOP-REAL n1;
A1: |. p1 .| = 1 by TOPREALB:12;
A2: |. -p1 .| = sqrt(|(-p1,-p1)|) by EUCLID_2:37
.= sqrt(|(p1,p1)|) by EUCLID_2:23
.= 1 by A1,EUCLID_2:37;
then |. -p1 + 0.TOP-REAL n1 .| = 1 by RLVECT_1:4;
then |. -p1 + (-1)*0.TOP-REAL n1 .| = 1 by RLVECT_1:10;
then B3: |. -p1 - 0.TOP-REAL n1 .| = 1 by RLVECT_1:16;
then
-p1 in Sphere(0.TOP-REAL n1,1) by TOPREAL9:9;
then -p1 in [#]((TOP-REAL n1) | Sphere(0.TOP-REAL n1,1))
by PRE_TOPC:def 5;
then -p1 in the carrier of Tcircle(0.TOP-REAL n1,1) by TOPREALB:def 6;
then -p1 in the carrier of Tunit_circle n1 by TOPREALB:def 7;
then reconsider A = {-p1} as Subset of M by ZFMISC_1:31;
reconsider U1 = [#]TUnitSphere(n)\A as Subset of M;
|. 0.TOP-REAL n1 .| <> |. -p1 .| by A2,EUCLID_2:39;
then 0.TOP-REAL n1 <> (1+1)*(-p1) by RLVECT_1:11;
then 0.TOP-REAL n1 <> 1*(-p1) + 1*(-p1) by RLVECT_1:def 6;
then 0.TOP-REAL n1 <> 1*(-p1) + -p1 by RLVECT_1:def 8;
then 0.TOP-REAL n1 <> -p1 + -p1 by RLVECT_1:def 8;
then -p1 + --p1 <> -p1 + -p1 by RLVECT_1:5;
then
A4: not p1 in {-p1} by TARSKI:def 1;
then p1 in U1 by XBOOLE_0:def 5;
then reconsider U = U1 as a_neighborhood of p by CONNSP_2:3,FRECHET:4;
take U;
reconsider m=n+1 as Nat;
A5: M = Tcircle(0.TOP-REAL m,1) by TOPREALB:def 7
.= (TOP-REAL m) | Sphere(0.TOP-REAL m,1) by TOPREALB:def 6;
reconsider S = Sphere(0.TOP-REAL m,1) as Subset of TOP-REAL m;
reconsider U11 = U1 as Subset of (TOP-REAL m) | S by A5;
U1 c= [#]Tunit_circle m;
then
A6: U1 c= Sphere(0.TOP-REAL m,1) by A5,PRE_TOPC:def 5;
then reconsider V = U11 as non empty Subset of TOP-REAL m
by A4,XBOOLE_0:def 5,XBOOLE_1:1;
M | U = (TOP-REAL m) | V by A5,A6,PRE_TOPC:7;
then reconsider U2 = M|U as non empty SubSpace of TOP-REAL m;
reconsider p2 = -p1 as Point of TOP-REAL m;
p2 <> 0.TOP-REAL m by A2,EUCLID_2:39;
then
A7: TOP-REAL n, TPlane(p2,0.TOP-REAL m)
are_homeomorphic by Th29;
A8: (TOP-REAL n) | ([#]TOP-REAL n) = the TopStruct of TOP-REAL n
by TSEP_1:93;
A9: TOP-REAL n, the TopStruct of TOP-REAL n are_homeomorphic by YELLOW14:19;
[#]U2 = U by PRE_TOPC:def 5
.= (the carrier of Tcircle(0.TOP-REAL m,1))\{p2} by TOPREALB:def 7
.= ([#]((TOP-REAL m) | Sphere(0.TOP-REAL m,1)))\{p2} by TOPREALB:def 6
.= Sphere(0.TOP-REAL m,1) \ {p2} by PRE_TOPC:def 5;
then stereographic_projection(U2,p2) is being_homeomorphism
by B3,TOPREAL9:9,Th31;
then U2, TPlane(p2,0.TOP-REAL m) are_homeomorphic by T_0TOPSP:def 1;
then TOP-REAL n, U2 are_homeomorphic by A7,BORSUK_3:3;
hence U,[#]TOP-REAL n are_homeomorphic
by A8,METRIZTS:def 1,A9,BORSUK_3:3;
end;
hence thesis by MFOLD_1:14;
end;
cluster TUnitSphere(n) -> n-manifold;
correctness;
end;