:: General {F}ashoda {M}eet {T}heorem for Unit Circle
:: by Yatsuka Nakamura
::
:: Received June 24, 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, COMPLEX1, XXREAL_0, ARYTM_1, MCART_1,
SQUARE_1, ARYTM_3, CARD_1, REAL_1, XBOOLE_0, METRIC_1, SUBSET_1, TOPMETR,
TARSKI, XXREAL_1, STRUCT_0, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2,
RCOMP_1, SUPINF_2, TOPREAL1, JGRAPH_3, JGRAPH_4, PSCOMP_1, SEQ_4,
RLTOPSP1, JORDAN6, TOPREAL2, JORDAN5C, PCOMPS_1, VALUED_1, JORDAN3,
FUNCT_2;
notations ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, XBOOLE_0,
SUBSET_1, TARSKI, RELAT_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
SEQ_4, STRUCT_0, RLVECT_1, RLTOPSP1, EUCLID, TOPMETR, PCOMPS_1, COMPTS_1,
METRIC_1, SQUARE_1, RCOMP_1, PSCOMP_1, BINOP_1, PRE_TOPC, JGRAPH_3,
TOPREAL1, JORDAN5C, JORDAN6, TOPREAL2, JGRAPH_4, XXREAL_0;
constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TOPREAL1,
JORDAN5C, JORDAN6, JGRAPH_3, JGRAPH_4, PSCOMP_1, SEQ_4, BINOP_2,
PCOMPS_1, BINOP_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR,
TOPREAL1, BORSUK_3, COMPTS_1, XXREAL_2, SQUARE_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
theorem :: JGRAPH_5:1
for p being Point of TOP-REAL 2 st |.p.|<=1 holds -1<=p`1 & p`1<=
1 & -1<=p`2 & p`2<=1;
theorem :: JGRAPH_5:2
for p being Point of TOP-REAL 2 st |.p.|<=1 & p`1<>0 & p`2<>0
holds -1
=d & t1>=t2 & s1 in [.a,b.]
& s2 in [.a,b.] holds s1<=s2;
theorem :: JGRAPH_5:10
for n being Element of NAT holds -(0.TOP-REAL n)=0.TOP-REAL n;
begin :: Fashoda Meet Theorems for Circle in Special Case
theorem :: JGRAPH_5:11
for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real, O
,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is
continuous one-to-one & a <> b & c <> d & (f.O)`1=a & c <=(f.O)`2 & (f.O)`2 <=d
& (f.I)`1=b & c <=(f.I)`2 & (f.I)`2 <=d & (g.O)`2=c & a <=(g.O)`1 & (g.O)`1 <=b
& (g.I)`2=d & a <=(g.I)`1 & (g.I)`1 <=b & (for r being Point of I[01] holds (a
>=(f.r)`1 or (f.r)`1>=b or c >=(f.r)`2 or (f.r)`2>=d) & (a >=(g.r)`1 or (g.r)`1
>=b or c >=(g.r)`2 or (g.r)`2>=d)) holds rng f meets rng g;
theorem :: JGRAPH_5:12
for f being Function of I[01],TOP-REAL 2 st f is continuous
one-to-one ex f2 being Function of I[01],TOP-REAL 2 st f2.0=f.1 & f2.1=f.0 &
rng f2=rng f & f2 is continuous & f2 is one-to-one;
reserve p,q for Point of TOP-REAL 2;
theorem :: JGRAPH_5:13
for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN
being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is
continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|<=1}& KXP={q1
where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2
where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3
where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4
where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in
KXN & f.I in KXP & g.O in KYP & g.I in KYN & rng f c= C0 & rng g c= C0 holds
rng f meets rng g;
theorem :: JGRAPH_5:14
for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN
being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is
continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|>=1}& KXP={q1
where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2
where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3
where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4
where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in
KXN & f.I in KXP & g.O in KYN & g.I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g;
theorem :: JGRAPH_5:15
for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN
being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is
continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|>=1}& KXP={q1
where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2
where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3
where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4
where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in
KXN & f.I in KXP & g.O in KYP & g.I in KYN & rng f c= C0 & rng g c= C0 holds
rng f meets rng g;
theorem :: JGRAPH_5:16
for f,g being Function of I[01],TOP-REAL 2, C0 being Subset of
TOP-REAL 2 st C0={q: |.q.|>=1} & f is continuous one-to-one & g is continuous
one-to-one & f.0=|[-1,0]| & f.1=|[1,0]| & g.1=|[0,1]| & g.0=|[0,-1]| & rng f c=
C0 & rng g c= C0 holds rng f meets rng g;
theorem :: JGRAPH_5:17
for p1,p2,p3,p4 being Point of TOP-REAL 2, C0 being Subset of TOP-REAL
2 st C0={p: |.p.|>=1} & |.p1.|=1 & |.p2.|=1 & |.p3.|=1 & |.p4.|=1 & (ex h being
Function of TOP-REAL 2,TOP-REAL 2 st h is being_homeomorphism & h.:C0 c= C0 & h
.p1=|[-1,0]| & h.p2=|[0,1]| & h.p3=|[1,0]| & h.p4=|[0,-1]|) holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & f.0=p1 & f.1=p3 & g.0=p4 & g.1=p2 & rng f c= C0 & rng g c= C0
holds rng f meets rng g;
begin :: Properties of Fan Morphisms
theorem :: JGRAPH_5:18
for cn being Real,q being Point of TOP-REAL 2 st -10 holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0
;
theorem :: JGRAPH_5:19
for cn being Real,q being Point of TOP-REAL 2 st -1=0
holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>=0;
theorem :: JGRAPH_5:20
for cn being Real,q being Point of TOP-REAL 2 st -1=0 & q`1/|.q.|0 holds for p being Point of TOP-REAL 2 st p=(cn
-FanMorphN).q holds p`2>=0 & p`1<0;
theorem :: JGRAPH_5:21
for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1=0 & q2`2>=0 & |.q1.|<>0 & |.q2.|<>0 & q1`1/|.q1.|0 holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0
;
theorem :: JGRAPH_5:23
for sn being Real,q being Point of TOP-REAL 2 st -1=0
& q`2/|.q.|0 holds for p being Point of TOP-REAL 2 st p=(sn
-FanMorphE).q holds p`1>=0 & p`2<0;
theorem :: JGRAPH_5:24
for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1=0 & q2`1>=0 & |.q1.|<>0 & |.q2.|<>0 & q1`2/|.q1.|cn holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).
q holds p`2<0 & p`1>0;
theorem :: JGRAPH_5:27
for cn being Real,q1,q2 being Point of TOP-REAL 2 st -10 & |.q2.|<>0 & q1`1/|.q1.|=0};
theorem :: JGRAPH_5:35
for P being compact non empty Subset of TOP-REAL 2 st P={q where
q is Point of TOP-REAL 2: |.q.|=1} holds Lower_Arc(P)={p where p is Point of
TOP-REAL 2:p in P & p`2<=0};
theorem :: JGRAPH_5:36
for a,b,d,e being Real st a<=b & e>0 ex f being Function of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(e*a+d,e*b+d) st f is
being_homeomorphism &
for r being Real st r in [.a,b.] holds f.r=e*r+d;
theorem :: JGRAPH_5:37
for a,b,d,e being Real st a<=b & e<0 ex f being Function of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(e*b+d,e*a+d) st f is
being_homeomorphism &
for r being Real st r in [.a,b.] holds f.r=e*r+d;
theorem :: JGRAPH_5:38
ex f being Function of I[01],Closed-Interval-TSpace(-1,1) st f
is being_homeomorphism &
(for r being Real st r in [.0,1.] holds f.r=(-2)*r+1)
& f.0=1 & f.1=-1;
theorem :: JGRAPH_5:39
ex f being Function of I[01],Closed-Interval-TSpace(-1,1) st f
is being_homeomorphism & (for r being Real st r in [.0,1.] holds f.r=2*r-1) & f
.0=-1 & f.1=1;
theorem :: JGRAPH_5:40
for P being compact non empty Subset of TOP-REAL 2 st P={p where
p is Point of TOP-REAL 2: |.p.|=1} ex f being Function of
Closed-Interval-TSpace(-1,1),(TOP-REAL 2)|Lower_Arc(P) st f is
being_homeomorphism & (for q being Point of TOP-REAL 2 st q in Lower_Arc(P)
holds f.(q`1)=q) & f.(-1)=W-min(P) & f.1=E-max(P);
theorem :: JGRAPH_5:41
for P being compact non empty Subset of TOP-REAL 2 st P={p where
p is Point of TOP-REAL 2: |.p.|=1} ex f being Function of
Closed-Interval-TSpace(-1,1),(TOP-REAL 2)|Upper_Arc(P) st f is
being_homeomorphism & (for q being Point of TOP-REAL 2 st q in Upper_Arc(P)
holds f.(q`1)=q) & f.(-1)=W-min(P) & f.1=E-max(P);
theorem :: JGRAPH_5:42
for P being compact non empty Subset of TOP-REAL 2 st P={p where
p is Point of TOP-REAL 2: |.p.|=1} ex f being Function of I[01],(TOP-REAL 2)|
Lower_Arc(P) st f is being_homeomorphism & (for q1,q2 being Point of TOP-REAL 2
, r1,r2 being Real st f.r1=q1 & f.r2=q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
r1q2`1)& f.0 = E-max(P) & f.1 = W-min(P);
theorem :: JGRAPH_5:43
for P being compact non empty Subset of TOP-REAL 2 st P={p where
p is Point of TOP-REAL 2: |.p.|=1} ex f being Function of I[01],(TOP-REAL 2)|
Upper_Arc(P) st f is being_homeomorphism & (for q1,q2 being Point of TOP-REAL 2
, r1,r2 being Real st f.r1=q1 & f.r2=q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
r1p2 & p1`1<0 & p1`2<0 & p2`2<0 holds p1`1>p2`1 & p1`2p2 & p2`1<0 & p1`2>=0 & p2`2>=0 holds p1`1p2 & p2`2>=0 holds p1`1p2 & p1`2<=0 & p1<>W-min(P) holds p1`1>p2`1;
theorem :: JGRAPH_5:49
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & (p2`2>=
0 or p2`1>=0) & LE p1,p2,P holds p1`2>=0 or p1`1>=0;
theorem :: JGRAPH_5:50
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & LE p1,
p2,P & p1<>p2 & p1`1>=0 & p2`1>=0 holds p1`2>p2`2;
theorem :: JGRAPH_5:51
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p1 in P
& p2 in P & p1`1<0 & p2`1<0 & p1`2<0 & p2`2<0 & (p1`1>=p2`1 or p1`2<=p2`2)
holds LE p1,p2,P;
theorem :: JGRAPH_5:52
for p1,p2 being Point of TOP-REAL 2, P being compact non empty Subset
of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p1 in P & p2
in P & p1`1>0 & p2`1>0 & p1`2<0 & p2`2<0 & (p1`1>=p2`1 or p1`2>=p2`2) holds LE
p1,p2,P;
theorem :: JGRAPH_5:53
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p1 in P
& p2 in P & p1`1<0 & p2`1<0 & p1`2>=0 & p2`2>=0 & (p1`1<=p2`1 or p1`2<=p2`2)
holds LE p1,p2,P;
theorem :: JGRAPH_5:54
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p1 in P
& p2 in P & p1`2>=0 & p2`2>=0 & p1`1<=p2`1 holds LE p1,p2,P;
theorem :: JGRAPH_5:55
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p1 in P
& p2 in P & p1`1>=0 & p2`1>=0 & p1`2>=p2`2 holds LE p1,p2,P;
theorem :: JGRAPH_5:56
for p1,p2 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p1 in P
& p2 in P & p1`2<=0 & p2`2<=0 & p2<>W-min(P) & p1`1>=p2`1 holds LE p1,p2,P;
theorem :: JGRAPH_5:57
for cn being Real,q being Point of TOP-REAL 2 st -1=0 & p2`1<0 & p2`2>=0 & p3
`1<0 & p3`2>=0 & p4`1<0 & p4`2>=0 ex f being Function of TOP-REAL 2,TOP-REAL 2,
q1,q2,q3,q4 being Point of TOP-REAL 2 st f is being_homeomorphism & (for q
being Point of TOP-REAL 2 holds |.(f.q).|=|.q.|)& q1=f.p1 & q2=f.p2 & q3=f.p3 &
q4=f.p4 & q1`1<0 & q1`2<0 & q2`1<0 & q2`2<0 & q3`1<0 & q3`2<0 & q4`1<0 & q4`2<0
& LE q1,q2,P & LE q2,q3,P & LE q3,q4,P;
theorem :: JGRAPH_5:60
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1`2>=0 & p2`2>=0 & p3`2>=0 & p4`2>0 ex
f being Function of TOP-REAL 2,TOP-REAL 2, q1,q2,q3,q4 being Point of TOP-REAL
2 st f is being_homeomorphism & (for q being Point of TOP-REAL 2 holds |.(f.q)
.|=|.q.|)& q1=f.p1 & q2=f.p2 & q3=f.p3 & q4=f.p4 & q1`1<0 & q1`2>=0 & q2`1<0 &
q2`2>=0 & q3`1<0 & q3`2>=0 & q4`1<0 & q4`2>=0 & LE q1,q2,P & LE q2,q3,P & LE q3
,q4,P;
theorem :: JGRAPH_5:61
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1`2>=0 & p2`2>=0 & p3`2>=0 & p4`2>0 ex
f being Function of TOP-REAL 2,TOP-REAL 2, q1,q2,q3,q4 being Point of TOP-REAL
2 st f is being_homeomorphism & (for q being Point of TOP-REAL 2 holds |.(f.q)
.|=|.q.|)& q1=f.p1 & q2=f.p2 & q3=f.p3 & q4=f.p4 & q1`1<0 & q1`2<0 & q2`1<0 &
q2`2<0 & q3`1<0 & q3`2<0 & q4`1<0 & q4`2<0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4
,P;
theorem :: JGRAPH_5:62
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & (p1`2>=0 or p1`1>=0)& (p2`2>=0 or p2`1>=
0) & (p3`2>=0 or p3`1>=0)& (p4`2>0 or p4`1>0) ex f being Function of TOP-REAL 2
,TOP-REAL 2, q1,q2,q3,q4 being Point of TOP-REAL 2 st f is being_homeomorphism
& (for q being Point of TOP-REAL 2 holds |.(f.q).|=|.q.|)& q1=f.p1 & q2=f.p2 &
q3=f.p3 & q4=f.p4 & q1`2>=0 & q2`2>=0 & q3`2>=0 & q4`2>0 & LE q1,q2,P & LE q2,
q3,P & LE q3,q4,P;
theorem :: JGRAPH_5:63
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & (p1`2>=0 or p1`1>=0)& (p2`2>=0 or p2`1>=
0) & (p3`2>=0 or p3`1>=0)& (p4`2>0 or p4`1>0) ex f being Function of TOP-REAL 2
,TOP-REAL 2, q1,q2,q3,q4 being Point of TOP-REAL 2 st f is being_homeomorphism
& (for q being Point of TOP-REAL 2 holds |.(f.q).|=|.q.|)& q1=f.p1 & q2=f.p2 &
q3=f.p3 & q4=f.p4 & q1`1<0 & q1`2<0 & q2`1<0 & q2`2<0 & q3`1<0 & q3`2<0 & q4`1<
0 & q4`2<0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P;
theorem :: JGRAPH_5:64
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} & p4=
W-min(P) & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ex f being Function of TOP-REAL
2,TOP-REAL 2, q1,q2,q3,q4 being Point of TOP-REAL 2 st f is being_homeomorphism
& (for q being Point of TOP-REAL 2 holds |.(f.q).|=|.q.|)& q1=f.p1 & q2=f.p2 &
q3=f.p3 & q4=f.p4 & q1`1<0 & q1`2<0 & q2`1<0 & q2`2<0 & q3`1<0 & q3`2<0 & q4`1<
0 & q4`2<0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P;
theorem :: JGRAPH_5:65
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ex f being Function of TOP-REAL 2,TOP-REAL
2, q1,q2,q3,q4 being Point of TOP-REAL 2 st f is being_homeomorphism & (for q
being Point of TOP-REAL 2 holds |.(f.q).|=|.q.|)& q1=f.p1 & q2=f.p2 & q3=f.p3 &
q4=f.p4 & q1`1<0 & q1`2<0 & q2`1<0 & q2`2<0 & q3`1<0 & q3`2<0 & q4`1<0 & q4`2<0
& LE q1,q2,P & LE q2,q3,P & LE q3,q4,P;
begin :: General Fashoda Meet Theorems
theorem :: JGRAPH_5:66
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1<>p2 & p2<>p3 & p3<>p4 & p1`1<0 & p2`1
<0 & p3`1<0 & p4`1<0 & p1`2<0 & p2`2<0 & p3`2<0 ex f being Function of TOP-REAL
2,TOP-REAL 2 st f is being_homeomorphism & (for q being Point of TOP-REAL 2
holds |.(f.q).|=|.q.|)& |[-1,0]|=f.p1 & |[0,1]|=f.p2 & |[1,0]|=f.p3 & |[0,-1]|=
f.p4;
theorem :: JGRAPH_5:67
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non
empty Subset of TOP-REAL 2 st P={p where p is Point of TOP-REAL 2: |.p.|=1} &
LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1<>p2 & p2<>p3 & p3<>p4 ex f being
Function of TOP-REAL 2,TOP-REAL 2 st f is being_homeomorphism & (for q being
Point of TOP-REAL 2 holds |.(f.q).|=|.q.|)& |[-1,0]|=f.p1 & |[0,1]|=f.p2 & |[1,
0]|=f.p3 & |[0,-1]|=f.p4;
theorem :: JGRAPH_5:68
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2 st P={p where p is Point of
TOP-REAL 2: |.p.|=1} & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & C0={p: |.p.|<=1}& f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & rng f c= C0
& rng g c= C0 holds rng f meets rng g;
theorem :: JGRAPH_5:69
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2 st P={p where p is Point of
TOP-REAL 2: |.p.|=1} & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & C0={p: |.p.|<=1}& f.0=p1 & f.1=p3 & g.0=p4 & g.1=p2 & rng f c= C0
& rng g c= C0 holds rng f meets rng g;
theorem :: JGRAPH_5:70
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2 st P={p where p is Point of
TOP-REAL 2: |.p.|=1} & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & C0={p: |.p.|>=1}& f.0=p1 & f.1=p3 & g.0=p4 & g.1=p2 & rng f c= C0
& rng g c= C0 holds rng f meets rng g;
theorem :: JGRAPH_5:71
for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty
Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2 st P={p where p is Point of
TOP-REAL 2: |.p.|=1} & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & C0={p: |.p.|>=1}& f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & rng f c= C0
& rng g c= C0 holds rng f meets rng g;