Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

The abstract of the Mizar article:

General Fashoda Meet Theorem for Unit Circle

by
Yatsuka Nakamura

Received June 24, 2002

MML identifier: JGRAPH_5
[ Mizar article, MML identifier index ]


environ

 vocabulary FUNCT_1, BOOLE, ABSVALUE, EUCLID, PRE_TOPC, SQUARE_1, RELAT_1,
      SUBSET_1, ARYTM_3, METRIC_1, RCOMP_1, FUNCT_5, TOPMETR, COMPTS_1,
      JGRAPH_4, ORDINAL2, TOPS_2, ARYTM_1, COMPLEX1, MCART_1, PCOMPS_1,
      JGRAPH_3, BORSUK_1, TOPREAL1, TOPREAL2, JORDAN3, PSCOMP_1, REALSET1,
      JORDAN5C, JORDAN6, ARYTM, SEQ_1;
 notation ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XBOOLE_0, ABSVALUE,
      EUCLID, TARSKI, RELAT_1, TOPS_2, FUNCT_1, FUNCT_2, NAT_1, STRUCT_0,
      TOPMETR, PCOMPS_1, COMPTS_1, METRIC_1, SQUARE_1, RCOMP_1, PSCOMP_1,
      BINOP_1, PRE_TOPC, JGRAPH_1, JGRAPH_3, TOPREAL1, JORDAN5C, JORDAN6,
      TOPREAL2, JGRAPH_4, GRCAT_1;
 constructors REAL_1, ABSVALUE, TOPREAL1, TOPS_2, RCOMP_1, PSCOMP_1, TOPREAL2,
      WELLFND1, JGRAPH_3, JORDAN5C, JORDAN6, JGRAPH_4, GRCAT_1, BORSUK_3,
      TOPRNS_1;
 clusters XREAL_0, STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR,
      SQUARE_1, PSCOMP_1, BORSUK_1, METRIC_1, BORSUK_2, BORSUK_3, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve x,a for real number;

theorem :: JGRAPH_5:1
  a>=0 & (x-a)*(x+a)>=0 implies -a>=x or x>=a;

theorem :: JGRAPH_5:2
a<=0 & x<a implies x^2>a^2;

theorem :: JGRAPH_5:3
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:4
for p being Point of TOP-REAL 2 st |.p.|<=1 & p`1<>0 & p`2<>0
 holds -1<p`1 & p`1<1 & -1<p`2 & p`2<1;

theorem :: JGRAPH_5:5
for a,b,d,e,r3 being Real,PM,PM2 being non empty MetrStruct,
 x being Element of PM,
 x2 being Element of PM2
 st d<=a & a<=b & b<=e
 & PM=Closed-Interval-MSpace(a,b)
 & PM2=Closed-Interval-MSpace(d,e)
 & x=x2 & x in the carrier of PM & x2 in the carrier of PM2
 holds Ball(x,r3) c= Ball(x2,r3);

theorem :: JGRAPH_5:6
for a,b,d,e being real number,
 B being Subset of Closed-Interval-TSpace(d,e)
 st d<=a & a<=b & b<=e & B=[.a,b.] holds
 Closed-Interval-TSpace(a,b)=Closed-Interval-TSpace(d,e)|B;

theorem :: JGRAPH_5:7
for a,b being real number, B being Subset of I[01]
 st 0<=a & a<=b & b<=1 & B=[.a,b.] holds
 Closed-Interval-TSpace(a,b)=I[01]|B;

theorem :: JGRAPH_5:8
for X being TopStruct,
 Y,Z being non empty TopStruct,f being map of X,Y,
 h being map of Y,Z st h is_homeomorphism & f is continuous
 holds h*f is continuous;

theorem :: JGRAPH_5:9
for X,Y,Z being TopStruct, f being map of X,Y,
 h being map of Y,Z st h is_homeomorphism & f is one-to-one
 holds h*f is one-to-one;

theorem :: JGRAPH_5:10
for X being TopStruct,S,V being non empty TopStruct,
 B being non empty Subset of S,f being map of X,S|B, g being map of S,V,
 h being map of X,V
 st h=g*f & f is continuous & g is continuous holds h is continuous;

theorem :: JGRAPH_5:11
for a,b,d,e,s1,s2,t1,t2 being Real,h being map of
 Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(d,e) st
 h is_homeomorphism & h.s1=t1 & h.s2=t2 & h.a=d & h.b=e & d<=e &
 t1<=t2 & s1 in [.a,b.] & s2 in [.a,b.] holds s1<=s2;

theorem :: JGRAPH_5:12
for a,b,d,e,s1,s2,t1,t2 being Real,h being map of
 Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(d,e) st
 h is_homeomorphism & h.s1=t1 & h.s2=t2 & h.a=e & h.b=d & e>=d &
 t1>=t2 & s1 in [.a,b.] & s2 in [.a,b.] holds s1<=s2;

theorem :: JGRAPH_5:13
for n being Nat holds
 -(0.REAL n)=0.REAL n;

begin :: Fashoda Meet Theorems for Circle in Special Case

theorem :: JGRAPH_5:14
 for f,g being map 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:15
for f being map of I[01],TOP-REAL 2 st
  f is continuous one-to-one
  ex f2 being map 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:16
for f,g being map 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:17
for f,g being map 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:18
for f,g being map 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:19
 for f,g being map 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:20
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 map of TOP-REAL 2,TOP-REAL 2 st h is_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 map 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:21
 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>0
 holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0);

theorem :: JGRAPH_5:22
   for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>=0
 holds (for p being Point of TOP-REAL 2 st
 p=(cn-FanMorphN).q holds p`2>=0);

theorem :: JGRAPH_5:23
 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>=0
 & q`1/|.q.|<cn & |.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:24
 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2>=0
 & q2`2>=0 & |.q1.|<>0 & |.q2.|<>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_5:25
 for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>0
 holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0);

theorem :: JGRAPH_5:26
   for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>=0
 & q`2/|.q.|<sn & |.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:27
 for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1>=0
 & q2`1>=0 & |.q1.|<>0 & |.q2.|<>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_5:28
 for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2<0
 holds (for p being Point of TOP-REAL 2 st
 p=(cn-FanMorphS).q holds p`2<0);

theorem :: JGRAPH_5:29
 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_5:30
 for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2<=0
 & q2`2<=0 & |.q1.|<>0 & |.q2.|<>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.|);

begin

theorem :: JGRAPH_5:31
for P being compact non empty Subset of TOP-REAL 2 st
 P={q: |.q.|=1}
 holds W-bound(P)=-1 & E-bound(P)=1 & S-bound(P)=-1 & N-bound(P)=1;

theorem :: JGRAPH_5:32
for P being compact non empty Subset of TOP-REAL 2 st
 P={q: |.q.|=1}
 holds W-min(P)=|[-1,0]|;

theorem :: JGRAPH_5:33
for P being compact non empty Subset of TOP-REAL 2 st
 P={q: |.q.|=1}
 holds E-max(P)=|[1,0]|;

theorem :: JGRAPH_5:34
  for f being map of TOP-REAL 2,R^1 st
(for p being Point of TOP-REAL 2 holds f.p=proj1.p) holds f is continuous;

theorem :: JGRAPH_5:35
for f being map of TOP-REAL 2,R^1 st
(for p being Point of TOP-REAL 2 holds f.p=proj2.p) holds f is continuous;

theorem :: JGRAPH_5:36
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
 Upper_Arc(P) c= P & Lower_Arc(P) c= P;

theorem :: JGRAPH_5:37
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
Upper_Arc(P)={p where p is Point of TOP-REAL 2:p in P & p`2>=0};

theorem :: JGRAPH_5:38
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:39
for a,b,d,e being Real st a<=b & e>0
  ex f being map of
     Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(e*a+d,e*b+d)
  st f is_homeomorphism & for r being Real st r in [.a,b.] holds
  f.r=e*r+d;

theorem :: JGRAPH_5:40
for a,b,d,e being Real st a<=b & e<0
  ex f being map of
     Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(e*b+d,e*a+d)
  st f is_homeomorphism & for r being Real st r in [.a,b.] holds
  f.r=e*r+d;

theorem :: JGRAPH_5:41
  ex f being map of I[01],Closed-Interval-TSpace(-1,1)
  st f is_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:42
  ex f being map of I[01],Closed-Interval-TSpace(-1,1)
  st f is_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: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 map of
     Closed-Interval-TSpace(-1,1),(TOP-REAL 2)|Lower_Arc(P)
  st f is_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:44
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 map of
     Closed-Interval-TSpace(-1,1),(TOP-REAL 2)|Upper_Arc(P)
  st f is_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:45
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 map of I[01],(TOP-REAL 2)|Lower_Arc(P)
  st f is_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 r1<r2 iff q1`1>q2`1)&
  f.0 = E-max(P) & f.1 = W-min(P);

theorem :: JGRAPH_5:46
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 map of I[01],(TOP-REAL 2)|Upper_Arc(P)
  st f is_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 r1<r2 iff q1`1<q2`1)&
  f.0 = W-min(P) & f.1 = E-max(P);

theorem :: JGRAPH_5:47
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 in Upper_Arc(P) & LE p1,p2,P
holds p1 in Upper_Arc(P);

theorem :: JGRAPH_5:48
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 & p1`2<0 & p2`2<0
 holds p1`1>p2`1 & p1`2<p2`2;

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}
 & LE p1,p2,P & p1<>p2 & p1`1<0 & p2`1<0 & p1`2>=0 & p2`2>=0
 holds p1`1<p2`1 & p1`2<p2`2;

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`2>=0 & p2`2>=0
 holds p1`1<p2`1;

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}
 & LE p1,p2,P & p1<>p2 & p1`2<=0 & p2`2<=0 & p1<>W-min(P)
 holds p1`1>p2`1;

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}
  & (p2`2>=0 or p2`1>=0) & LE p1,p2,P
holds p1`2>=0 or p1`1>=0;

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}
 & LE p1,p2,P & p1<>p2 & p1`1>=0 & p2`1>=0
 holds p1`2>p2`2;

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`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: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<0 & p2`2<0 &
 (p1`1>=p2`1 or 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`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:57
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:58
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:59
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:60
for cn being Real,q being Point of TOP-REAL 2 st
  -1<cn & cn<1 & q`2<=0 holds (for p being Point of TOP-REAL 2 st
 p=(cn-FanMorphS).q holds p`2<=0);

theorem :: JGRAPH_5:61
for cn being Real,p1,p2,q1,q2 being Point of TOP-REAL 2,
 P being compact non empty Subset of TOP-REAL 2
 st -1<cn & cn<1 & P={p where p is Point of TOP-REAL 2: |.p.|=1}
 & LE p1,p2,P & q1=(cn-FanMorphS).p1 & q2=(cn-FanMorphS).p2
 holds LE q1,q2,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`1<0 & p1`2>=0 & p2`1<0 & p2`2>=0
  & p3`1<0 & p3`2>=0 & p4`1<0 & p4`2>=0
 ex f being map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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: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 & p2`2>=0
  & p3`2>=0 & p4`2>0
 ex f being map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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}
 & 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 map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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
  & (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 map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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: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`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 map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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: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}
 & p4=W-min(P) & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P
 ex f being map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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:68
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 map of TOP-REAL 2,TOP-REAL 2,
   q1,q2,q3,q4 being Point of TOP-REAL 2 st
   f is_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:69
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 & p4`2<0
 ex f being map of TOP-REAL 2,TOP-REAL 2 st
   f is_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:70
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 map of TOP-REAL 2,TOP-REAL 2 st
   f is_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: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 map 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:72
  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 map 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:73
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 map 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:74
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 map 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);

Back to top