Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Fan Homeomorphisms in the Plane

**by****Yatsuka Nakamura**- Received January 8, 2002
- MML identifier: JGRAPH_4

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, BOOLE, ABSVALUE, EUCLID, PRE_TOPC, JORDAN2C, SQUARE_1, RELAT_1, SUBSET_1, ARYTM_3, METRIC_1, RCOMP_1, FUNCT_4, FUNCT_5, TOPMETR, COMPTS_1, JGRAPH_4, ORDINAL2, TOPS_2, ARYTM_1, CARD_3, COMPLEX1, MCART_1, PARTFUN1, PCOMPS_1, LATTICES, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, STRUCT_0, PARTFUN1, TOPMETR, PCOMPS_1, EUCLID, COMPTS_1, TOPS_2, METRIC_1, SQUARE_1, TBSP_1, RCOMP_1, PSCOMP_1, PRE_TOPC, JGRAPH_1, JORDAN2C, FUNCT_4; constructors REAL_1, TOPS_2, TBSP_1, RCOMP_1, PSCOMP_1, JORDAN2C, COMPTS_1, TOPGRP_1, TOPMETR, WELLFND1, TOPRNS_1, MEMBERED; clusters XREAL_0, STRUCT_0, RELSET_1, EUCLID, PRE_TOPC, SQUARE_1, PSCOMP_1, METRIC_1, TOPREAL6, BORSUK_2, JORDAN6, MEMBERED, ZFMISC_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve x,a for real number; reserve p,q for Point of TOP-REAL 2; canceled; theorem :: JGRAPH_4:2 a>=0 & (x-a)*(x+a)<0 implies -a<x & x<a; theorem :: JGRAPH_4:3 for sn being real number st -1<sn & sn<1 holds 1+sn>0 & 1-sn>0; theorem :: JGRAPH_4:4 for a being real number st a^2<=1 holds -1<=a & a<=1; theorem :: JGRAPH_4:5 for a being real number st a^2<1 holds -1<a & a<1; theorem :: JGRAPH_4:6 for X being non empty TopStruct, g being map of X,R^1, B being Subset of X, a being real number st g is continuous & B = {p where p is Point of X: pi(g,p) > a } holds B is open; theorem :: JGRAPH_4:7 for X being non empty TopStruct, g being map of X,R^1,B being Subset of X, a being Real st g is continuous & B={p where p is Point of X: pi(g,p) < a } holds B is open; theorem :: JGRAPH_4:8 for f being map of TOP-REAL 2,TOP-REAL 2 st f is continuous one-to-one & rng f=[#](TOP-REAL 2) & (for p2 being Point of TOP-REAL 2 ex K being non empty compact Subset of TOP-REAL 2 st K = f.:K & (ex V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & f.p2 in V2)) holds f is_homeomorphism; theorem :: JGRAPH_4:9 for X being non empty TopSpace, f1,f2 being map of X,R^1,a,b being real number st f1 is continuous & f2 is continuous & b<>0 & (for q being Point of X holds f2.q<>0) holds ex g being map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p=(r1/r2-a)/b) & g is continuous; theorem :: JGRAPH_4:10 for X being non empty TopSpace, f1,f2 being map of X,R^1,a,b being Real st f1 is continuous & f2 is continuous & b<>0 & (for q being Point of X holds f2.q<>0) holds ex g being map of X,R^1 st (for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r2*((r1/r2-a)/b)) & g is continuous; theorem :: JGRAPH_4:11 for X being non empty TopSpace, f1 being map of X,R^1 st f1 is continuous holds ex g being map of X,R^1 st (for p being Point of X,r1 being real number st f1.p=r1 holds g.p=r1^2) & g is continuous; theorem :: JGRAPH_4:12 for X being non empty TopSpace, f1 being map of X,R^1 st f1 is continuous holds ex g being map of X,R^1 st (for p being Point of X,r1 being real number st f1.p=r1 holds g.p=abs(r1)) & g is continuous; theorem :: JGRAPH_4:13 for X being non empty TopSpace, f1 being map of X,R^1 st f1 is continuous holds ex g being map of X,R^1 st (for p being Point of X,r1 being real number st f1.p=r1 holds g.p=-r1) & g is continuous; theorem :: JGRAPH_4:14 for X being non empty TopSpace, f1,f2 being map of X,R^1,a,b being real number st f1 is continuous & f2 is continuous & b<>0 & (for q being Point of X holds f2.q<>0) holds ex g being map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p= r2*(-sqrt(abs(1-((r1/r2-a)/b)^2)))) & g is continuous; theorem :: JGRAPH_4:15 for X being non empty TopSpace, f1,f2 being map of X,R^1,a,b being real number st f1 is continuous & f2 is continuous & b<>0 & (for q being Point of X holds f2.q<>0) holds ex g being map of X,R^1 st (for p being Point of X,r1,r2 being real number st f1.p=r1 & f2.p=r2 holds g.p= r2*( sqrt(abs(1-((r1/r2-a)/b)^2)))) & g is continuous; definition let n be Nat; func n NormF -> Function of the carrier of TOP-REAL n, the carrier of R^1 means :: JGRAPH_4:def 1 for q being Point of TOP-REAL n holds it.q=|.q.|; end; theorem :: JGRAPH_4:16 for n being Nat holds dom (n NormF)=the carrier of TOP-REAL n & dom (n NormF)=REAL n; canceled 2; theorem :: JGRAPH_4:19 for n being Nat,f being map of TOP-REAL n,R^1 st f=n NormF holds f is continuous; theorem :: JGRAPH_4:20 for n being Nat,K0 being Subset of TOP-REAL n, f being map of (TOP-REAL n)|K0,R^1 st (for p being Point of (TOP-REAL n)|K0 holds f.p=(n NormF).p) holds f is continuous; theorem :: JGRAPH_4:21 for n being Nat,p being Point of Euclid n,r being Real, B being Subset of TOP-REAL n st B=cl_Ball(p,r) holds B is Bounded & B is closed; theorem :: JGRAPH_4:22 for p being Point of Euclid 2,r being Real, B being Subset of TOP-REAL 2 st B=cl_Ball(p,r) holds B is compact; begin :: Fan Morphism for West definition let s be real number, q be Point of TOP-REAL 2; func FanW(s,q) -> Point of TOP-REAL 2 equals :: JGRAPH_4:def 2 |.q.|*|[-sqrt(1-((q`2/|.q.|-s)/(1-s))^2), (q`2/|.q.|-s)/(1-s)]| if q`2/|.q.|>=s & q`1<0, |.q.|*|[-sqrt(1-((q`2/|.q.|-s)/(1+s))^2), (q`2/|.q.|-s)/(1+s)]| if q`2/|.q.|<s & q`1<0 otherwise q; end; definition let s be real number; func s-FanMorphW -> Function of the carrier of TOP-REAL 2, the carrier of TOP-REAL 2 means :: JGRAPH_4:def 3 for q being Point of TOP-REAL 2 holds it.q=FanW(s,q); end; theorem :: JGRAPH_4:23 for sn being real number holds (q`2/|.q.|>=sn & q`1<0 implies sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)), |.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) & (q`1>=0 implies sn-FanMorphW.q=q); theorem :: JGRAPH_4:24 for sn being Real holds (q`2/|.q.|<=sn & q`1<0 implies sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|); theorem :: JGRAPH_4:25 for sn being Real st -1<sn & sn<1 holds (q`2/|.q.|>=sn & q`1<=0 & q<>0.REAL 2 implies sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)), |.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) & (q`2/|.q.|<=sn & q`1<=0 & q<>0.REAL 2 implies sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|); theorem :: JGRAPH_4:26 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:27 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:28 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q`2/|.q.|>=sn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:29 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q`2/|.q.|<=sn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:30 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.REAL 2} & K0={p: p`2/|.p.|>=sn & p`1<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:31 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.REAL 2} & K0={p: p`2/|.p.|<=sn & p`1<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:32 for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2>=(sn)*(|.p.|) & p`1<=0} holds K03 is closed; theorem :: JGRAPH_4:33 for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2<=(sn)*(|.p.|) & p`1<=0} holds K03 is closed; theorem :: JGRAPH_4:34 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:35 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:36 for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2)|B0 st B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1<=0 & p<>0.REAL 2} holds K0 is closed; theorem :: JGRAPH_4:37 for sn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:38 for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2)|B0 st B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1>=0 & p<>0.REAL 2} holds K0 is closed; theorem :: JGRAPH_4:39 for sn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:40 for sn being Real,p being Point of TOP-REAL 2 holds |.(sn-FanMorphW).p.|=|.p.|; theorem :: JGRAPH_4:41 for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0={p: p`1<=0 & p<>0.REAL 2} holds (sn-FanMorphW).x in K0; theorem :: JGRAPH_4:42 for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0={p: p`1>=0 & p<>0.REAL 2} holds (sn-FanMorphW).x in K0; theorem :: JGRAPH_4:43 for sn being Real, D being non empty Subset of TOP-REAL 2 st -1<sn & sn<1 & D`={0.REAL 2} holds ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(sn-FanMorphW)|D & h is continuous; theorem :: JGRAPH_4:44 for sn being Real st -1<sn & sn<1 holds ex h being map of (TOP-REAL 2),(TOP-REAL 2) st h=(sn-FanMorphW) & h is continuous; theorem :: JGRAPH_4:45 for sn being Real st -1<sn & sn<1 holds (sn-FanMorphW) is one-to-one; theorem :: JGRAPH_4:46 for sn being Real st -1<sn & sn<1 holds (sn-FanMorphW) is map of TOP-REAL 2,TOP-REAL 2 & rng (sn-FanMorphW) = the carrier of TOP-REAL 2; theorem :: JGRAPH_4:47 for sn being Real,p2 being Point of TOP-REAL 2 st -1<sn & sn<1 ex K being non empty compact Subset of TOP-REAL 2 st K = (sn-FanMorphW).:K & (ex V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (sn-FanMorphW).p2 in V2); theorem :: JGRAPH_4:48 for sn being Real st -1<sn & sn<1 ex f being map of TOP-REAL 2,TOP-REAL 2 st f=(sn-FanMorphW) & f is_homeomorphism; theorem :: JGRAPH_4:49 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1<0 & q`2/|.q.|>=sn holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphW).q holds p`1<0 & p`2>=0); theorem :: JGRAPH_4:50 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1<0 & q`2/|.q.|<sn holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphW).q holds p`1<0 & p`2<0); theorem :: JGRAPH_4:51 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1<0 & q1`2/|.q1.|>=sn & q2`1<0 & q2`2/|.q2.|>=sn & q1`2/|.q1.|<q2`2/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphW).q1 & p2=(sn-FanMorphW).q2 holds p1`2/|.p1.|<p2`2/|.p2.|); theorem :: JGRAPH_4:52 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1<0 & q1`2/|.q1.|<sn & q2`1<0 & q2`2/|.q2.|<sn & q1`2/|.q1.|<q2`2/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphW).q1 & p2=(sn-FanMorphW).q2 holds p1`2/|.p1.|<p2`2/|.p2.|); theorem :: JGRAPH_4:53 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1<0 & q2`1<0 & q1`2/|.q1.|<q2`2/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphW).q1 & p2=(sn-FanMorphW).q2 holds p1`2/|.p1.|<p2`2/|.p2.|); theorem :: JGRAPH_4:54 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1<0 & q`2/|.q.|=sn holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphW).q holds p`1<0 & p`2=0); theorem :: JGRAPH_4:55 for sn being real number holds 0.REAL 2=(sn-FanMorphW).(0.REAL 2); begin :: Fan Morphism for North definition let s be real number, q be Point of TOP-REAL 2; func FanN(s,q) -> Point of TOP-REAL 2 equals :: JGRAPH_4:def 4 |.q.|*|[(q`1/|.q.|-s)/(1-s), sqrt(1-((q`1/|.q.|-s)/(1-s))^2)]| if q`1/|.q.|>=s & q`2>0, |.q.|*|[(q`1/|.q.|-s)/(1+s), sqrt(1-((q`1/|.q.|-s)/(1+s))^2)]| if q`1/|.q.|<s & q`2>0 otherwise q; end; definition let c be real number; func c-FanMorphN -> Function of the carrier of TOP-REAL 2, the carrier of TOP-REAL 2 means :: JGRAPH_4:def 5 for q being Point of TOP-REAL 2 holds it.q=FanN(c,q); end; theorem :: JGRAPH_4:56 for cn being real number holds (q`1/|.q.|>=cn & q`2>0 implies cn-FanMorphN.q= |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)), |.q.|*(sqrt(1-((q`1/|.q.|-cn)/(1-cn))^2))]|)& (q`2<=0 implies cn-FanMorphN.q=q); theorem :: JGRAPH_4:57 for cn being Real holds (q`1/|.q.|<=cn & q`2>0 implies cn-FanMorphN.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*( sqrt(1-((q`1/|.q.|-cn)/(1+cn))^2))]|); theorem :: JGRAPH_4:58 for cn being Real st -1<cn & cn<1 holds (q`1/|.q.|>=cn & q`2>=0 & q<>0.REAL 2 implies cn-FanMorphN.q= |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)), |.q.|*( sqrt(1-((q`1/|.q.|-cn)/(1-cn))^2))]|) & (q`1/|.q.|<=cn & q`2>=0 & q<>0.REAL 2 implies cn-FanMorphN.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*( sqrt(1-((q`1/|.q.|-cn)/(1+cn))^2))]|); theorem :: JGRAPH_4:59 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|-cn)/(1-cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2>=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:60 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|-cn)/(1+cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2>=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:61 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( sqrt(1-((p`1/|.p.|-cn)/(1-cn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2>=0 & q`1/|.q.|>=cn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:62 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( sqrt(1-((p`1/|.p.|-cn)/(1+cn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2>=0 & q`1/|.q.|<=cn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:63 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0={q where q is Point of TOP-REAL 2: q`2>=0 & q<>0.REAL 2} & K0={p: p`1/|.p.|>=cn & p`2>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:64 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0={q where q is Point of TOP-REAL 2: q`2>=0 & q<>0.REAL 2} & K0={p: p`1/|.p.|<=cn & p`2>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:65 for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`1>=(cn)*(|.p.|) & p`2>=0} holds K03 is closed; theorem :: JGRAPH_4:66 for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`1<=(cn)*(|.p.|) & p`2>=0} holds K03 is closed; theorem :: JGRAPH_4:67 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:68 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:69 for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2)|B0 st B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2>=0 & p<>0.REAL 2} holds K0 is closed; theorem :: JGRAPH_4:70 for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2)|B0 st B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2<=0 & p<>0.REAL 2} holds K0 is closed; theorem :: JGRAPH_4:71 for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:72 for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:73 for cn being Real,p being Point of TOP-REAL 2 holds |.(cn-FanMorphN).p.|=|.p.|; theorem :: JGRAPH_4:74 for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0={p: p`2>=0 & p<>0.REAL 2} holds (cn-FanMorphN).x in K0; theorem :: JGRAPH_4:75 for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0={p: p`2<=0 & p<>0.REAL 2} holds (cn-FanMorphN).x in K0; theorem :: JGRAPH_4:76 for cn being Real, D being non empty Subset of TOP-REAL 2 st -1<cn & cn<1 & D`={0.REAL 2} holds ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(cn-FanMorphN)|D & h is continuous; theorem :: JGRAPH_4:77 for cn being Real st -1<cn & cn<1 holds ex h being map of (TOP-REAL 2),(TOP-REAL 2) st h=(cn-FanMorphN) & h is continuous; theorem :: JGRAPH_4:78 for cn being Real st -1<cn & cn<1 holds (cn-FanMorphN) is one-to-one; theorem :: JGRAPH_4:79 for cn being Real st -1<cn & cn<1 holds (cn-FanMorphN) is map of TOP-REAL 2,TOP-REAL 2 & rng (cn-FanMorphN) = the carrier of TOP-REAL 2; theorem :: JGRAPH_4:80 for cn being Real,p2 being Point of TOP-REAL 2 st -1<cn & cn<1 ex K being non empty compact Subset of TOP-REAL 2 st K = (cn-FanMorphN).:K & (ex V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (cn-FanMorphN).p2 in V2); theorem :: JGRAPH_4:81 for cn being Real st -1<cn & cn<1 ex f being map of TOP-REAL 2,TOP-REAL 2 st f=(cn-FanMorphN) & f is_homeomorphism; theorem :: JGRAPH_4:82 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>0 & q`1/|.q.|>=cn holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0 & p`1>=0); theorem :: JGRAPH_4:83 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>0 & q`1/|.q.|<cn holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0 & p`1<0); theorem :: JGRAPH_4:84 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2>0 & q1`1/|.q1.|>=cn & q2`2>0 & q2`1/|.q2.|>=cn & q1`1/|.q1.|<q2`1/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds p1`1/|.p1.|<p2`1/|.p2.|); theorem :: JGRAPH_4:85 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2>0 & q1`1/|.q1.|<cn & q2`2>0 & q2`1/|.q2.|<cn & q1`1/|.q1.|<q2`1/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds p1`1/|.p1.|<p2`1/|.p2.|); theorem :: JGRAPH_4:86 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2>0 & q2`2>0 & q1`1/|.q1.|<q2`1/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds p1`1/|.p1.|<p2`1/|.p2.|); theorem :: JGRAPH_4:87 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>0 & q`1/|.q.|=cn holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0 & p`1=0); theorem :: JGRAPH_4:88 for cn being real number holds 0.REAL 2=(cn-FanMorphN).(0.REAL 2); begin :: Fan Morphism for East definition let s be real number, q be Point of TOP-REAL 2; func FanE(s,q) -> Point of TOP-REAL 2 equals :: JGRAPH_4:def 6 |.q.|*|[sqrt(1-((q`2/|.q.|-s)/(1-s))^2), (q`2/|.q.|-s)/(1-s)]| if q`2/|.q.|>=s & q`1>0, |.q.|*|[sqrt(1-((q`2/|.q.|-s)/(1+s))^2), (q`2/|.q.|-s)/(1+s)]| if q`2/|.q.|<s & q`1>0 otherwise q; end; definition let s be real number; func s-FanMorphE -> Function of the carrier of TOP-REAL 2, the carrier of TOP-REAL 2 means :: JGRAPH_4:def 7 for q being Point of TOP-REAL 2 holds it.q=FanE(s,q); end; theorem :: JGRAPH_4:89 for sn being real number holds (q`2/|.q.|>=sn & q`1>0 implies sn-FanMorphE.q= |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)), |.q.|* ((q`2/|.q.|-sn)/(1-sn))]|)& (q`1<=0 implies sn-FanMorphE.q=q); theorem :: JGRAPH_4:90 for sn being Real holds (q`2/|.q.|<=sn & q`1>0 implies sn-FanMorphE.q= |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|); theorem :: JGRAPH_4:91 for sn being Real st -1<sn & sn<1 holds (q`2/|.q.|>=sn & q`1>=0 & q<>0.REAL 2 implies sn-FanMorphE.q= |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)), |.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) & (q`2/|.q.|<=sn & q`1>=0 & q<>0.REAL 2 implies sn-FanMorphE.q= |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|); theorem :: JGRAPH_4:92 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1-sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1>=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:93 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1+sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1>=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:94 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(sqrt(1-((p`2/|.p.|-sn)/(1-sn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1>=0 & q`2/|.q.|>=sn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:95 for sn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<sn & sn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(sqrt(1-((p`2/|.p.|-sn)/(1+sn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`1>=0 & q`2/|.q.|<=sn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:96 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0={q where q is Point of TOP-REAL 2: q`1>=0 & q<>0.REAL 2} & K0={p: p`2/|.p.|>=sn & p`1>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:97 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0={q where q is Point of TOP-REAL 2: q`1>=0 & q<>0.REAL 2} & K0={p: p`2/|.p.|<=sn & p`1>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:98 for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2>=(sn)*(|.p.|) & p`1>=0} holds K03 is closed; theorem :: JGRAPH_4:99 for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2<=(sn)*(|.p.|) & p`1>=0} holds K03 is closed; theorem :: JGRAPH_4:100 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:101 for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:102 for sn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:103 for sn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`1<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:104 for sn being Real,p being Point of TOP-REAL 2 holds |.(sn-FanMorphE).p.|=|.p.|; theorem :: JGRAPH_4:105 for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0={p: p`1>=0 & p<>0.REAL 2} holds (sn-FanMorphE).x in K0; theorem :: JGRAPH_4:106 for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0={p: p`1<=0 & p<>0.REAL 2} holds (sn-FanMorphE).x in K0; theorem :: JGRAPH_4:107 for sn being Real, D being non empty Subset of TOP-REAL 2 st -1<sn & sn<1 & D`={0.REAL 2} holds ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(sn-FanMorphE)|D & h is continuous; theorem :: JGRAPH_4:108 for sn being Real st -1<sn & sn<1 holds ex h being map of (TOP-REAL 2),(TOP-REAL 2) st h=(sn-FanMorphE) & h is continuous; theorem :: JGRAPH_4:109 for sn being Real st -1<sn & sn<1 holds (sn-FanMorphE) is one-to-one; theorem :: JGRAPH_4:110 for sn being Real st -1<sn & sn<1 holds (sn-FanMorphE) is map of TOP-REAL 2,TOP-REAL 2 & rng (sn-FanMorphE) = the carrier of TOP-REAL 2; theorem :: JGRAPH_4:111 for sn being Real,p2 being Point of TOP-REAL 2 st -1<sn & sn<1 ex K being non empty compact Subset of TOP-REAL 2 st K = (sn-FanMorphE).:K & (ex V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (sn-FanMorphE).p2 in V2); theorem :: JGRAPH_4:112 for sn being Real st -1<sn & sn<1 ex f being map of TOP-REAL 2,TOP-REAL 2 st f=(sn-FanMorphE) & f is_homeomorphism; theorem :: JGRAPH_4:113 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>0 & q`2/|.q.|>=sn holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0 & p`2>=0); theorem :: JGRAPH_4:114 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>0 & q`2/|.q.|<sn holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0 & p`2<0); theorem :: JGRAPH_4:115 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1>0 & q1`2/|.q1.|>=sn & q2`1>0 & q2`2/|.q2.|>=sn & q1`2/|.q1.|<q2`2/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds p1`2/|.p1.|<p2`2/|.p2.|); theorem :: JGRAPH_4:116 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1>0 & q1`2/|.q1.|<sn & q2`1>0 & q2`2/|.q2.|<sn & q1`2/|.q1.|<q2`2/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds p1`2/|.p1.|<p2`2/|.p2.|); theorem :: JGRAPH_4:117 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1>0 & q2`1>0 & q1`2/|.q1.|<q2`2/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds p1`2/|.p1.|<p2`2/|.p2.|); theorem :: JGRAPH_4:118 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>0 & q`2/|.q.|=sn holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0 & p`2=0); theorem :: JGRAPH_4:119 for sn being real number holds 0.REAL 2=(sn-FanMorphE).(0.REAL 2); begin :: Fan Morphism for South definition let s be real number, q be Point of TOP-REAL 2; func FanS(s,q) -> Point of TOP-REAL 2 equals :: JGRAPH_4:def 8 |.q.|*|[(q`1/|.q.|-s)/(1-s), -sqrt(1-((q`1/|.q.|-s)/(1-s))^2)]| if q`1/|.q.|>=s & q`2<0, |.q.|*|[(q`1/|.q.|-s)/(1+s), -sqrt(1-((q`1/|.q.|-s)/(1+s))^2)]| if q`1/|.q.|<s & q`2<0 otherwise q; end; definition let c be real number; func c-FanMorphS -> Function of the carrier of TOP-REAL 2, the carrier of TOP-REAL 2 means :: JGRAPH_4:def 9 for q being Point of TOP-REAL 2 holds it.q=FanS(c,q); end; theorem :: JGRAPH_4:120 for cn being real number holds (q`1/|.q.|>=cn & q`2<0 implies cn-FanMorphS.q= |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)), |.q.|*(-sqrt(1-((q`1/|.q.|-cn)/(1-cn))^2))]|)& (q`2>=0 implies cn-FanMorphS.q=q); theorem :: JGRAPH_4:121 for cn being Real holds (q`1/|.q.|<=cn & q`2<0 implies cn-FanMorphS.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*( -sqrt(1-((q`1/|.q.|-cn)/(1+cn))^2))]|); theorem :: JGRAPH_4:122 for cn being Real st -1<cn & cn<1 holds (q`1/|.q.|>=cn & q`2<=0 & q<>0.REAL 2 implies cn-FanMorphS.q= |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)), |.q.|*( -sqrt(1-((q`1/|.q.|-cn)/(1-cn))^2))]|) & (q`1/|.q.|<=cn & q`2<=0 & q<>0.REAL 2 implies cn-FanMorphS.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*( -sqrt(1-((q`1/|.q.|-cn)/(1+cn))^2))]|); theorem :: JGRAPH_4:123 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|-cn)/(1-cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:124 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|-cn)/(1+cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<=0 & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:125 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( -sqrt(1-((p`1/|.p.|-cn)/(1-cn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<=0 & q`1/|.q.|>=cn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:126 for cn being Real,K1 being non empty Subset of TOP-REAL 2, f being map of (TOP-REAL 2)|K1,R^1 st -1<cn & cn<1 & (for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( -sqrt(1-((p`1/|.p.|-cn)/(1+cn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1 holds q`2<=0 & q`1/|.q.|<=cn & q<>0.REAL 2) holds f is continuous; theorem :: JGRAPH_4:127 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0={q where q is Point of TOP-REAL 2: q`2<=0 & q<>0.REAL 2} & K0={p: p`1/|.p.|>=cn & p`2<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:128 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0={q where q is Point of TOP-REAL 2: q`2<=0 & q<>0.REAL 2} & K0={p: p`1/|.p.|<=cn & p`2<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:129 for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`1>=(cn)*(|.p.|) & p`2<=0} holds K03 is closed; theorem :: JGRAPH_4:130 for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`1<=(cn)*(|.p.|) & p`2<=0} holds K03 is closed; theorem :: JGRAPH_4:131 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:132 for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:133 for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2<=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:134 for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2)|B0,f being map of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} & K0={p: p`2>=0 & p<>0.REAL 2} holds f is continuous; theorem :: JGRAPH_4:135 for cn being Real,p being Point of TOP-REAL 2 holds |.(cn-FanMorphS).p.|=|.p.|; theorem :: JGRAPH_4:136 for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0={p: p`2<=0 & p<>0.REAL 2} holds (cn-FanMorphS).x in K0; theorem :: JGRAPH_4:137 for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0={p: p`2>=0 & p<>0.REAL 2} holds (cn-FanMorphS).x in K0; theorem :: JGRAPH_4:138 for cn being Real, D being non empty Subset of TOP-REAL 2 st -1<cn & cn<1 & D`={0.REAL 2} holds ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(cn-FanMorphS)|D & h is continuous; theorem :: JGRAPH_4:139 for cn being Real st -1<cn & cn<1 holds ex h being map of (TOP-REAL 2),(TOP-REAL 2) st h=(cn-FanMorphS) & h is continuous; theorem :: JGRAPH_4:140 for cn being Real st -1<cn & cn<1 holds cn-FanMorphS is one-to-one; theorem :: JGRAPH_4:141 for cn being Real st -1<cn & cn<1 holds (cn-FanMorphS) is map of TOP-REAL 2,TOP-REAL 2 & rng (cn-FanMorphS) = the carrier of TOP-REAL 2; theorem :: JGRAPH_4:142 for cn being Real,p2 being Point of TOP-REAL 2 st -1<cn & cn<1 ex K being non empty compact Subset of TOP-REAL 2 st K = (cn-FanMorphS).:K & (ex V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (cn-FanMorphS).p2 in V2); theorem :: JGRAPH_4:143 for cn being Real st -1<cn & cn<1 ex f being map of TOP-REAL 2,TOP-REAL 2 st f=cn-FanMorphS & f is_homeomorphism; theorem :: JGRAPH_4:144 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2<0 & q`1/|.q.|>=cn holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).q holds p`2<0 & p`1>=0); theorem :: JGRAPH_4:145 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2<0 & q`1/|.q.|<cn holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).q holds p`2<0 & p`1<0); theorem :: JGRAPH_4:146 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2<0 & q1`1/|.q1.|>=cn & q2`2<0 & q2`1/|.q2.|>=cn & q1`1/|.q1.|<q2`1/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds p1`1/|.p1.|<p2`1/|.p2.|); theorem :: JGRAPH_4:147 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2<0 & q1`1/|.q1.|<cn & q2`2<0 & q2`1/|.q2.|<cn & q1`1/|.q1.|<q2`1/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds p1`1/|.p1.|<p2`1/|.p2.|); theorem :: JGRAPH_4:148 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2<0 & q2`2<0 & q1`1/|.q1.|<q2`1/|.q2.| holds (for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds p1`1/|.p1.|<p2`1/|.p2.|); theorem :: JGRAPH_4:149 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2<0 & q`1/|.q.|=cn holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).q holds p`2<0 & p`1=0); theorem :: JGRAPH_4:150 for cn being real number holds 0.REAL 2=(cn-FanMorphS).(0.REAL 2);

Back to top