Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

The abstract of the Mizar article:

On the Simple Closed Curve Property of the Circle and the Fashoda Meet Theorem for It

by
Yatsuka Nakamura

Received August 20, 2001

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


environ

 vocabulary ARYTM, SQUARE_1, EUCLID, PCOMPS_1, RELAT_1, FUNCT_5, PRE_TOPC,
      MCART_1, ARYTM_1, ARYTM_3, RCOMP_1, COMPLEX1, FUNCT_1, BOOLE, SUBSET_1,
      COMPTS_1, ORDINAL2, TOPMETR, JORDAN2C, FUNCT_4, PARTFUN1, METRIC_1,
      TOPS_2, TOPREAL2, TOPREAL1, BORSUK_1, JGRAPH_3, SEQ_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, EUCLID, RELAT_1, TOPS_2, FUNCT_1, STRUCT_0, PARTFUN1, TOPREAL1,
      TOPMETR, PCOMPS_1, COMPTS_1, METRIC_1, RCOMP_1, SQUARE_1, FUNCT_2,
      PSCOMP_1, PRE_TOPC, JGRAPH_1, JORDAN2C, FUNCT_4, WELLFND1, TOPREAL2,
      TOPGRP_1;
 constructors REAL_1, GOBOARD5, TOPS_2, RCOMP_1, PSCOMP_1, JORDAN2C, COMPTS_1,
      TOPREAL2, TOPGRP_1, CONNSP_1, TOPMETR, WELLFND1, TOPRNS_1;
 clusters XREAL_0, STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, SQUARE_1,
      BORSUK_1, TOPREAL2, TOPREAL6, BORSUK_2, BORSUK_3, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin ::Preliminaries

reserve x,y,z,u,a for real number;

theorem :: JGRAPH_3:1
x^2=y^2 implies x=y or x=-y;

theorem :: JGRAPH_3:2
x^2=1 implies x=1 or x=-1;

theorem :: JGRAPH_3:3
0<=x & x<=1 implies x^2<=x;

theorem :: JGRAPH_3:4
a>=0 & (x-a)*(x+a)<=0 implies -a<=x & x<=a;

theorem :: JGRAPH_3:5
x^2-1<=0 implies -1<=x & x<=1;

theorem :: JGRAPH_3:6
 x < y & x < z iff x < min(y,z);

theorem :: JGRAPH_3:7
0<x implies x/3<x & x/4<x;

theorem :: JGRAPH_3:8
(x>=1 implies sqrt x>=1) & (x>1 implies sqrt x>1);

theorem :: JGRAPH_3:9
x<=y & z<=u implies ].y,z.[ c= ].x,u.[;

theorem :: JGRAPH_3:10
for p being Point of TOP-REAL 2 holds
 |.p.| = sqrt((p`1)^2+(p`2)^2) &
 |.p.|^2 = (p`1)^2+(p`2)^2;

theorem :: JGRAPH_3:11
for f being Function,B,C being set holds (f|B).:C = f.:(C /\ B);

theorem :: JGRAPH_3:12
for X being TopStruct,Y being non empty TopStruct,
 f being map of X,Y,
 P being Subset of X holds f|P is map of X|P,Y;

theorem :: JGRAPH_3:13
for X,Y being non empty TopSpace,
  p0 being Point of X,
  D being non empty Subset of X,
  E being non empty Subset of Y,
  f being map of X,Y
 st D`={p0} & E`={f.p0} & X is_T2 & Y is_T2 &
 (for p being Point of X|D holds f.p<>f.p0)&
 (ex h being map of X|D,Y|E st h=f|D & h is continuous) &
 (for V being Subset of Y st f.p0 in V & V is open
 ex W being Subset of X st p0 in W & W is open & f.:W c= V)
 holds f is continuous;

begin ::The Circle is a Simple Closed Curve

reserve p,q for Point of TOP-REAL 2;

definition
  func Sq_Circ -> Function of the carrier of TOP-REAL 2,
                              the carrier of TOP-REAL 2 means
:: JGRAPH_3:def 1
  for p being Point of TOP-REAL 2 holds
  (p=0.REAL 2 implies it.p=p) &
  ((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
  it.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|)&
  (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
  it.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|);
end;

theorem :: JGRAPH_3:14
for p being Point of TOP-REAL 2 st p<>0.REAL 2 holds
 ((p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)implies
 Sq_Circ.p=|[p`1/sqrt(1+(p`1/p`2)^2),p`2/sqrt(1+(p`1/p`2)^2)]|) &
 (not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies
 Sq_Circ.p=|[p`1/sqrt(1+(p`2/p`1)^2),p`2/sqrt(1+(p`2/p`1)^2)]|);

theorem :: JGRAPH_3:15
for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous &
(for q being Point of X ex r being real number st f1.q=r & r>=0)
 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=sqrt(r1)) & g is continuous;

theorem :: JGRAPH_3:16
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(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)^2) & g is continuous;

theorem :: JGRAPH_3:17
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(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=1+(r1/r2)^2) & g is continuous;

theorem :: JGRAPH_3:18
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(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=sqrt(1+(r1/r2)^2)) & g is continuous;

theorem :: JGRAPH_3:19
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(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/sqrt(1+(r1/r2)^2)) & g is continuous;

theorem :: JGRAPH_3:20
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(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(1+(r1/r2)^2)) & g is continuous;

theorem :: JGRAPH_3:21
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`1/sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:22
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`2/sqrt(1+(p`2/p`1)^2)) &
  (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:23
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`2/sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:24
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`1/sqrt(1+(p`1/p`2)^2)) &
  (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:25
for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous;

theorem :: JGRAPH_3:26
for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous;

scheme TopIncl { P[set] } :
  { p: P[p] & p<>0.REAL 2 } c= (the carrier of TOP-REAL 2) \ {0.REAL 2};

scheme TopInter { P[set] } :
  { p: P[p] & p<>0.REAL 2 } =
   { p7 where p7 is Point of TOP-REAL 2 : P[p7]} /\
   ((the carrier of TOP-REAL 2) \ {0.REAL 2});

theorem :: JGRAPH_3:27
for 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 f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous & K0 is closed;

theorem :: JGRAPH_3:28
for 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 f=Sq_Circ|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous & K0 is closed;

theorem :: JGRAPH_3:29
for D being non empty Subset of TOP-REAL 2
st D`={0.REAL 2} holds
ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
st h=Sq_Circ|D & h is continuous;

theorem :: JGRAPH_3:30
for D being non empty Subset of TOP-REAL 2 st
    D=(the carrier of TOP-REAL 2) \ {0.REAL 2} holds D`= {0.REAL 2};

theorem :: JGRAPH_3:31
ex h being map of TOP-REAL 2, TOP-REAL 2 st h=Sq_Circ & h is continuous;

theorem :: JGRAPH_3:32
Sq_Circ is one-to-one;

definition
  cluster Sq_Circ -> one-to-one;
end;

theorem :: JGRAPH_3:33
for Kb,Cb being Subset of TOP-REAL 2 st
 Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
      or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}&
 Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|=1} holds Sq_Circ.:Kb=Cb;

theorem :: JGRAPH_3:34
for P,Kb being Subset of TOP-REAL 2,f being map of
 (TOP-REAL 2)|Kb,(TOP-REAL 2)|P st
 Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
      or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}
 & f is_homeomorphism
 holds P is_simple_closed_curve;

theorem :: JGRAPH_3:35
for Kb being Subset of TOP-REAL 2
 st Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
      or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}
 holds Kb is_simple_closed_curve & Kb is compact;

theorem :: JGRAPH_3:36
for Cb being Subset of TOP-REAL 2 st
  Cb={p where p is Point of TOP-REAL 2: |.p.|=1}
 holds Cb is_simple_closed_curve;

begin :: The Fashoda Meet Theorem for the Circle

theorem :: JGRAPH_3:37
for K0,C0 being Subset of TOP-REAL 2 st
 K0={p: -1<=p`1 & p`1<=1 & -1<=p`2 & p`2<=1}
& C0={p1 where p1 is Point of TOP-REAL 2: |.p1.|<=1}
holds Sq_Circ"(C0) c= K0;

theorem :: JGRAPH_3:38
for p holds
 (p=0.REAL 2 implies Sq_Circ".p=0.REAL 2) &
 ( (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2 implies
    Sq_Circ".p=|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2)]|)&
 (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)& p<>0.REAL 2 implies
    Sq_Circ".p=|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|);

theorem :: JGRAPH_3:39
Sq_Circ" is map of TOP-REAL 2,TOP-REAL 2;

theorem :: JGRAPH_3:40
for p being Point of TOP-REAL 2 st p<>0.REAL 2 holds
 ((p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies
 (Sq_Circ").p=|[p`1*sqrt(1+(p`1/p`2)^2),p`2*sqrt(1+(p`1/p`2)^2)]|) &
 (not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies
 (Sq_Circ").p=|[p`1*sqrt(1+(p`2/p`1)^2),p`2*sqrt(1+(p`2/p`1)^2)]|);

theorem :: JGRAPH_3:41
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(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*sqrt(1+(r1/r2)^2)) & g is continuous;

theorem :: JGRAPH_3:42
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous & f2 is continuous &
(for q being Point of X holds f2.q<>0)
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(1+(r1/r2)^2)) & g is continuous;

theorem :: JGRAPH_3:43
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`1*sqrt(1+(p`2/p`1)^2)) & (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:44
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`2*sqrt(1+(p`2/p`1)^2)) &
  (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`1<>0) holds f is continuous;

theorem :: JGRAPH_3:45
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`2*sqrt(1+(p`1/p`2)^2)) & (for q being Point of TOP-REAL 2 st
q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:46
for K1 being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K1,R^1 st
(for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
  holds f.p=p`1*sqrt(1+(p`1/p`2)^2)) &
  (for q being Point of TOP-REAL 2 st q in
  the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds
f is continuous;

theorem :: JGRAPH_3:47
for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous;

theorem :: JGRAPH_3:48
for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2} &
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous;

theorem :: JGRAPH_3:49
for 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 f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
holds f is continuous & K0 is closed;

theorem :: JGRAPH_3:50
for 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 f=(Sq_Circ")|K0 & B0=(the carrier of TOP-REAL 2) \ {0.REAL 2}
& K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
holds f is continuous & K0 is closed;

theorem :: JGRAPH_3:51
for D being non empty Subset of TOP-REAL 2
st D`={0.REAL 2} holds
ex h being map of (TOP-REAL 2)|D,(TOP-REAL 2)|D
st h=(Sq_Circ")|D & h is continuous;

theorem :: JGRAPH_3:52
ex h being map of TOP-REAL 2,TOP-REAL 2 st h=Sq_Circ" & h is continuous;

canceled;

theorem :: JGRAPH_3:54
Sq_Circ is map of TOP-REAL 2,TOP-REAL 2 &
 rng Sq_Circ = the carrier of TOP-REAL 2 &
 for f being map of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ holds
   f is_homeomorphism;

theorem :: JGRAPH_3:55
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;


Back to top