:: Fan Homeomorphisms in the Plane
:: by Yatsuka Nakamura
::
:: Received January 8, 2002
:: Copyright (c) 2002-2021 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, PRE_TOPC, EUCLID, SUPINF_2, COMPLEX1, XXREAL_0, CARD_1,
XBOOLE_0, FUNCT_1, TOPMETR, SUBSET_1, ORDINAL2, PARTFUN1, RCOMP_1,
REAL_1, TARSKI, STRUCT_0, RELAT_1, ARYTM_3, TOPS_2, ARYTM_1, SQUARE_1,
NAT_1, METRIC_1, XXREAL_2, PCOMPS_1, MCART_1, FUNCT_4, JGRAPH_4, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, COMPLEX1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1,
STRUCT_0, PARTFUN1, TOPMETR, RLVECT_1, EUCLID, COMPTS_1, TOPS_2,
METRIC_1, PCOMPS_1, SQUARE_1, TBSP_1, PSCOMP_1, PRE_TOPC, RLTOPSP1,
FUNCT_4, XXREAL_0;
constructors FUNCT_4, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, TOPS_2, COMPTS_1,
TBSP_1, TOPMETR, PSCOMP_1, FUNCSDOM, PCOMPS_1;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED,
STRUCT_0, PRE_TOPC, EUCLID, TOPMETR, TOPREAL1, PSCOMP_1, FUNCT_2,
COMPTS_1, TBSP_1, RELSET_1, FUNCT_1, JORDAN2C, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve a for Real;
reserve p,q for Point of TOP-REAL 2;
theorem :: JGRAPH_4:1
for X being non empty TopStruct, g being Function of X,R^1, B
being Subset of X, a being Real st g is continuous & B = {p where p is
Point of X: g/.p > a } holds B is open;
theorem :: JGRAPH_4:2
for X being non empty TopStruct, g being Function of X,R^1,B
being Subset of X,
a being Real st g is continuous & B={p where p is Point of X
: g/.p < a } holds B is open;
theorem :: JGRAPH_4:3
for f being Function 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
being_homeomorphism;
theorem :: JGRAPH_4:4
for X being non empty TopSpace, f1,f2 being Function 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 Function 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=(r1/r2-a)/b)
& g is continuous;
theorem :: JGRAPH_4:5
for X being non empty TopSpace, f1,f2 being Function 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 Function 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:6
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1
being Real st f1.p=r1 holds g.p=r1^2) & g is continuous;
theorem :: JGRAPH_4:7
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1
being Real st f1.p=r1 holds g.p=|.r1.|) & g is continuous;
theorem :: JGRAPH_4:8
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1
being Real st f1.p=r1 holds g.p=-r1) & g is continuous;
theorem :: JGRAPH_4:9
for X being non empty TopSpace, f1,f2 being Function 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 Function 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*(-
sqrt(|.1-((r1/r2-a)/b)^2.|))) & g is continuous;
theorem :: JGRAPH_4:10
for X being non empty TopSpace, f1,f2 being Function 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 Function 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*(
sqrt(|.1-((r1/r2-a)/b)^2.|))) & g is continuous;
definition
let n be Nat;
func n NormF -> Function of TOP-REAL n, R^1 means
:: JGRAPH_4:def 1
for q being Point of TOP-REAL n holds it.q=|.q.|;
end;
theorem :: JGRAPH_4:11
for n being Nat holds dom (n NormF)=the carrier of TOP-REAL
n & dom (n NormF)=REAL n;
theorem :: JGRAPH_4:12
for n being Nat holds n NormF is continuous;
registration
let n be Nat;
cluster n NormF -> continuous;
end;
theorem :: JGRAPH_4:13
for n being Element of NAT,K0 being Subset of TOP-REAL n, f
being Function 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:14
for n being Element of 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 closed;
theorem :: JGRAPH_4:15
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, 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.|~~ Function of TOP-REAL 2, 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:16
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))]|) & (q`1>=0 implies sn-FanMorphW.q=q);
theorem :: JGRAPH_4:17
for sn being Real st q`2/|.q.|<=sn & q`1<0 holds sn-FanMorphW.q=
|[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|;
theorem :: JGRAPH_4:18
for sn being Real st -1=sn & q`1<=0
& q<>0.TOP-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.
TOP-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:19
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:20
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -10.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:21
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is
continuous;
theorem :: JGRAPH_4:22
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -10.TOP-REAL 2)
holds f is continuous;
theorem :: JGRAPH_4:23
for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} & K0={p: p
`2/|.p.|>=sn & p`1<=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:24
for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} & K0={p: p
`2/|.p.|<=sn & p`1<=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:25
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:26
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:27
for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:28
for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:29
for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`1<=0 & p<>0.TOP-REAL 2} holds K0 is
closed;
theorem :: JGRAPH_4:30
for sn being Real, B0 being Subset of TOP-REAL 2, K0 being
Subset of (TOP-REAL 2)|B0, f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL
2)|B0) st -10.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:31
for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`1>=0 & p<>0.TOP-REAL 2} holds K0 is
closed;
theorem :: JGRAPH_4:32
for sn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset
of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st -1=0 &
p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:33
for sn being Real,p being Point of TOP-REAL 2 holds |.(sn
-FanMorphW).p.|=|.p.|;
theorem :: JGRAPH_4:34
for sn being Real,x,K0 being set st -10.TOP-REAL 2} holds (sn-FanMorphW).x in K0;
theorem :: JGRAPH_4:35
for sn being Real,x,K0 being set st -1=0 & p<>0.TOP-REAL 2} holds (sn-FanMorphW).x in K0;
scheme :: JGRAPH_4:sch 1
InclSub { D() -> non empty Subset of TOP-REAL 2, P[set] } : { p : P[p] & p<>
0.TOP-REAL 2 } c= the carrier of (TOP-REAL 2)|D()
provided
D() = NonZero TOP-REAL 2;
theorem :: JGRAPH_4:36
for sn being Real, D being non empty Subset of TOP-REAL 2 st -1<
sn & sn<1 & D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(
TOP-REAL 2)|D st h=(sn-FanMorphW)|D & h is continuous;
theorem :: JGRAPH_4:37
for sn being Real st -1=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:43
for sn being Real,q being Point of TOP-REAL 2 st -1=sn & q2`1<0 & q2`2/|.q2.|>=sn & q1`2/|.q1.| 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.|~~~~0
otherwise q;
end;
definition
let c be Real;
func c-FanMorphN -> Function of TOP-REAL 2, 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:49
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))]|)& (q`2<=0 implies cn-FanMorphN.q=q);
theorem :: JGRAPH_4:50
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:51
for cn being Real st -1=cn & q`2>=0
& q<>0.TOP-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.
TOP-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:52
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:53
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -1=0 & q<>0.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:54
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is
continuous;
theorem :: JGRAPH_4:55
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -1=0 & q`1/|.q.|<=cn & q<>0.TOP-REAL 2)
holds f is continuous;
theorem :: JGRAPH_4:56
for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & q<>0.TOP-REAL 2} & K0={p: p
`1/|.p.|>=cn & p`2>=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:57
for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & q<>0.TOP-REAL 2} & K0={p: p
`1/|.p.|<=cn & p`2>=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:58
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:59
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:60
for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:61
for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:62
for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`2>=0 & p<>0.TOP-REAL 2} holds K0 is
closed;
theorem :: JGRAPH_4:63
for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`2<=0 & p<>0.TOP-REAL 2} holds K0 is
closed;
theorem :: JGRAPH_4:64
for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset
of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st -1=0 &
p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:65
for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset
of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st -10.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:66
for cn being Real,p being Point of TOP-REAL 2 holds |.(cn
-FanMorphN).p.|=|.p.|;
theorem :: JGRAPH_4:67
for cn being Real,x,K0 being set st -1=0 & p<>0.TOP-REAL 2} holds (cn-FanMorphN).x in K0;
theorem :: JGRAPH_4:68
for cn being Real,x,K0 being set st -10.TOP-REAL 2} holds (cn-FanMorphN).x in K0;
theorem :: JGRAPH_4:69
for cn being Real, D being non empty Subset of TOP-REAL 2 st -1<
cn & cn<1 & D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(
TOP-REAL 2)|D st h=(cn-FanMorphN)|D & h is continuous;
theorem :: JGRAPH_4:70
for cn being Real st -10 &
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:76
for cn being Real,q being Point of TOP-REAL 2 st -10 &
q`1/|.q.|0 & p`1<0;
theorem :: JGRAPH_4:77
for cn being Real,q1,q2 being Point of TOP-REAL 2 st cn<1 & q1`2
>0 & q1`1/|.q1.|>=cn & q2`2>0 & q2`1/|.q2.|>=cn & q1`1/|.q1.|0 & q1`1/|.q1.|0 & q2`1/|.q2.| 0 & q2`2>0 & q1`1/|.q1.|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:81
for cn being Real holds 0.TOP-REAL 2=(cn-FanMorphN).(0.TOP-REAL
2);
begin :: Fan Morphism for East
definition
let s be Real, 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.|~~~~0
otherwise q;
end;
definition
let s be Real;
func s-FanMorphE -> Function of TOP-REAL 2, 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:82
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))]|)& (q`1<=0 implies sn-FanMorphE.q=q);
theorem :: JGRAPH_4:83
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:84
for sn being Real st -1=sn & q`1>=0
& q<>0.TOP-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.
TOP-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:85
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:86
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -1=0 & q<>0.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:87
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is
continuous;
theorem :: JGRAPH_4:88
for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -1=0 & q`2/|.q.|<=sn & q<>0.TOP-REAL 2)
holds f is continuous;
theorem :: JGRAPH_4:89
for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & q<>0.TOP-REAL 2} & K0={p: p
`2/|.p.|>=sn & p`1>=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:90
for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & q<>0.TOP-REAL 2} & K0={p: p
`2/|.p.|<=sn & p`1>=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:91
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:92
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:93
for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:94
for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:95
for sn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -1=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:96
for sn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -10.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:97
for sn being Real,p being Point of TOP-REAL 2 holds |.(sn
-FanMorphE).p.|=|.p.|;
theorem :: JGRAPH_4:98
for sn being Real,x,K0 being set st -1=0 & p<>0.TOP-REAL 2} holds (sn-FanMorphE).x in K0;
theorem :: JGRAPH_4:99
for sn being Real,x,K0 being set st -10.TOP-REAL 2} holds (sn-FanMorphE).x in K0;
theorem :: JGRAPH_4:100
for sn being Real, D being non empty Subset of TOP-REAL 2 st -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:107
for sn being Real,q being Point of TOP-REAL 2 st -10
& q`2/|.q.|0 & p`2<0;
theorem :: JGRAPH_4:108
for sn being Real,q1,q2 being Point of TOP-REAL 2 st sn<1 & q1
`1>0 & q1`2/|.q1.|>=sn & q2`1>0 & q2`2/|.q2.|>=sn & q1`2/|.q1.|0 & q1`2/|.q1.|0 & q2`2/|.q2.|0 & q2`1>0 & q1`2/|.q1.|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:112
for sn being Real holds 0.TOP-REAL 2=(sn-FanMorphE).(0.TOP-REAL
2);
begin :: Fan Morphism for South
definition
let s be Real, 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.|~~~~ Function of TOP-REAL 2, 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:113
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))]|)& (q`2>=0 implies cn-FanMorphS.q=q);
theorem :: JGRAPH_4:114
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:115
for cn being Real st -1=cn & q`2<=0
& q<>0.TOP-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.TOP-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:116
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:117
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -10.TOP-REAL 2) holds f is continuous;
theorem :: JGRAPH_4:118
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st 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.TOP-REAL 2) holds f is
continuous;
theorem :: JGRAPH_4:119
for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st -10.TOP-REAL 2)
holds f is continuous;
theorem :: JGRAPH_4:120
for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} & K0={p: p
`1/|.p.|>=cn & p`2<=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:121
for cn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} & K0={p: p
`1/|.p.|<=cn & p`2<=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:122
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:123
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:124
for cn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -10.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:125
for cn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1=0 & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_4:126
for cn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -10.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:127
for cn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -1=0 & p<>0.TOP-REAL 2} holds f is continuous;
theorem :: JGRAPH_4:128
for cn being Real,p being Point of TOP-REAL 2 holds |.(cn
-FanMorphS).p.|=|.p.|;
theorem :: JGRAPH_4:129
for cn being Real,x,K0 being set st -10.TOP-REAL 2} holds (cn-FanMorphS).x in K0;
theorem :: JGRAPH_4:130
for cn being Real,x,K0 being set st -1=0 & p<>0.TOP-REAL 2} holds (cn-FanMorphS).x in K0;
theorem :: JGRAPH_4:131
for cn being Real, D being non empty Subset of TOP-REAL 2 st -1
=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:138
for cn being Real,q being Point of TOP-REAL 2 st -1=cn & q2`2<0 & q2`1/|.q2.|>=cn & q1`1/|.q1.|~~