Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002
Association of Mizar Users
The abstract of the Mizar article:
-
- 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