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