:: On the Simple Closed Curve Property of the Circle and the
:: Fashoda Meet Theorem for It
:: by Yatsuka Nakamura
::
:: Received August 20, 2001
:: Copyright (c) 2001-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, SQUARE_1, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, STRUCT_0,
EUCLID, PRE_TOPC, COMPLEX1, MCART_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
ORDINAL2, RCOMP_1, SUPINF_2, ARYTM_1, TOPMETR, REAL_1, XXREAL_1,
JORDAN2C, FUNCT_4, PARTFUN1, PCOMPS_1, METRIC_1, TOPS_2, TOPREAL2,
TOPREAL1, VALUED_1, BORSUK_1, JGRAPH_3, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, RLVECT_1, EUCLID, RELAT_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, DOMAIN_1, STRUCT_0, TOPREAL1, TOPMETR, COMPTS_1, METRIC_1,
RCOMP_1, SQUARE_1, PCOMPS_1, PSCOMP_1, PRE_TOPC, FUNCT_4, TOPREAL2,
XXREAL_0;
constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR,
TOPREAL1, TOPREAL2, PSCOMP_1, FUNCSDOM, PCOMPS_1;
registrations FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
SQUARE_1, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR,
TOPREAL1, TOPREAL2, BORSUK_3, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve x for Real;
theorem :: JGRAPH_3:1
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:2
for f being Function,B,C being set holds (f|B).:C = f.:(C /\ B);
theorem :: JGRAPH_3:3
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 Function of X,Y
st D`={p0} & E`={f.p0} & X is T_2 & Y is T_2 & (for p being Point of X|D holds
f.p<>f.p0)& f|D is continuous Function of X|D,Y|E & (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.TOP-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.
TOP-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.TOP-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:4
for p being Point of TOP-REAL 2 st p<>0.TOP-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:5
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous & (for q being Point of X ex r being Real st f1.q=r & r>=0
) holds ex g being Function of X,R^1 st (for p being Point of X,r1 being Real
st f1.p=r1 holds g.p=sqrt(r1)) & g is continuous;
theorem :: JGRAPH_3:6
for X being non empty TopSpace, f1,f2 being Function 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 Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=(r1/r2)^2) & g is continuous;
theorem :: JGRAPH_3:7
for X being non empty TopSpace, f1,f2 being Function 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 Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=1+(r1/r2)^2) & g is continuous;
theorem :: JGRAPH_3:8
for X being non empty TopSpace, f1,f2 being Function 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 Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=sqrt(1+(r1/r2)^2)) & g is continuous;
theorem :: JGRAPH_3:9
for X being non empty TopSpace, f1,f2 being Function 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 Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=r1/sqrt(1+(r1/r2)^2)) & g is continuous;
theorem :: JGRAPH_3:10
for X being non empty TopSpace, f1,f2 being Function 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 Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=r2/sqrt(1+(r1/r2)^2)) & g is continuous;
theorem :: JGRAPH_3:11
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:12
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:13
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:14
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:15
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Sq_Circ|K0 & B0=NonZero TOP-REAL 2 & K0={p:
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_3:16
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Sq_Circ|K0 & B0=NonZero TOP-REAL 2 & K0={p:
(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is
continuous;
scheme :: JGRAPH_3:sch 1
TopIncl { P[set] } : { p: P[p] & p<>0.TOP-REAL 2 } c= NonZero TOP-REAL 2;
scheme :: JGRAPH_3:sch 2
TopInter { P[set] } : { p: P[p] & p<>0.TOP-REAL 2 } = { p7 where p7 is Point
of TOP-REAL 2 : P[p7]} /\ (NonZero TOP-REAL 2);
theorem :: JGRAPH_3:17
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Sq_Circ|K0
& B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.TOP-REAL 2} holds f is continuous & K0 is closed;
theorem :: JGRAPH_3:18
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Sq_Circ|K0
& B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.TOP-REAL 2} holds f is continuous & K0 is closed;
theorem :: JGRAPH_3:19
for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2}
holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=Sq_Circ|D & h
is continuous;
theorem :: JGRAPH_3:20
for D being non empty Subset of TOP-REAL 2 st D=NonZero TOP-REAL
2 holds D`= {0.TOP-REAL 2};
theorem :: JGRAPH_3:21
ex h being Function of TOP-REAL 2, TOP-REAL 2 st h=Sq_Circ & h is continuous;
theorem :: JGRAPH_3:22
Sq_Circ is one-to-one;
registration
cluster Sq_Circ -> one-to-one;
end;
theorem :: JGRAPH_3:23
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:24
for P,Kb being Subset of TOP-REAL 2,f being Function 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
being_homeomorphism holds P is being_simple_closed_curve;
theorem :: JGRAPH_3:25
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 being_simple_closed_curve & Kb is compact;
theorem :: JGRAPH_3:26
for Cb being Subset of TOP-REAL 2 st Cb={p where p is Point of
TOP-REAL 2: |.p.|=1} holds Cb is being_simple_closed_curve;
begin :: The Fashoda Meet Theorem for the Circle
theorem :: JGRAPH_3:27
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:28
for p holds (p=0.TOP-REAL 2 implies Sq_Circ".p=0.TOP-REAL 2) & (
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-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) 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:29
Sq_Circ" is Function of TOP-REAL 2,TOP-REAL 2;
theorem :: JGRAPH_3:30
for p being Point of TOP-REAL 2 st p<>0.TOP-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:31
for X being non empty TopSpace, f1,f2 being Function 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 Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=r1*sqrt(1+(r1/r2)^2)) & g is continuous;
theorem :: JGRAPH_3:32
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0) ex
g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real st
f1.p=r1 & f2.p=r2 holds g.p=r2*sqrt(1+(r1/r2)^2)) & g is continuous;
theorem :: JGRAPH_3:33
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:34
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:35
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:36
for K1 being non empty Subset of TOP-REAL 2, f being Function 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:37
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0=
{p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_3:38
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=(Sq_Circ")|K0 & B0=NonZero TOP-REAL 2 & K0=
{p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is
continuous;
theorem :: JGRAPH_3:39
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ")
|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p
`1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed;
theorem :: JGRAPH_3:40
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=(Sq_Circ")
|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p
`2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed;
theorem :: JGRAPH_3:41
for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2}
holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=(Sq_Circ")|D &
h is continuous;
theorem :: JGRAPH_3:42
ex h being Function of TOP-REAL 2,TOP-REAL 2 st h=Sq_Circ" & h is continuous;
theorem :: JGRAPH_3:43
Sq_Circ is Function of TOP-REAL 2,TOP-REAL 2 & rng Sq_Circ = the
carrier of TOP-REAL 2 & for f being Function of TOP-REAL 2,TOP-REAL 2 st f=
Sq_Circ holds f is being_homeomorphism;
theorem :: JGRAPH_3:44
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;