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 July 16, 2001
- MML identifier: JGRAPH_2
- [
Mizar article,
MML identifier index
]
environ
vocabulary EUCLID, PCOMPS_1, ARYTM, ARYTM_3, RELAT_1, SQUARE_1, ARYTM_1,
PRE_TOPC, SUBSET_1, BOOLE, ORDINAL2, FUNCT_1, FUNCT_4, METRIC_1,
COMPLEX1, MCART_1, JORDAN2C, FINSEQ_1, FINSEQ_2, FUNCT_5, TOPMETR,
RCOMP_1, PARTFUN1, BORSUK_1, JGRAPH_2;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, NAT_1, STRUCT_0, PARTFUN1,
PRE_TOPC, TOPMETR, PCOMPS_1, METRIC_1, RCOMP_1, FUNCT_2, SQUARE_1,
PSCOMP_1, EUCLID, JGRAPH_1, JORDAN2C, FUNCT_4, WELLFND1;
constructors REAL_1, WEIERSTR, TOPS_2, RCOMP_1, PSCOMP_1, JORDAN2C, WELLFND1,
FUNCT_4, TOPRNS_1, MEMBERED;
clusters SUBSET_1, STRUCT_0, RELSET_1, EUCLID, PRE_TOPC, TOPMETR, SQUARE_1,
PSCOMP_1, BORSUK_1, XREAL_0, ARYTM_3, MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
canceled;
theorem :: JGRAPH_2:2
for a being real number st 1 <= a holds a <= a^2;
theorem :: JGRAPH_2:3
for a being real number st -1 >= a holds -a <= a^2;
theorem :: JGRAPH_2:4
for a being real number st -1 > a holds -a < a^2;
theorem :: JGRAPH_2:5
for a,b being real number st b^2<= a^2 & a>=0 holds
-a<=b & b<=a;
theorem :: JGRAPH_2:6
for a,b being real number st b^2< a^2 & a>=0 holds
-a<b & b<a;
theorem :: JGRAPH_2:7
for a,b being real number st
-a<=b & b<=a holds b^2<= a^2;
theorem :: JGRAPH_2:8
for a,b being real number st
-a<b & b<a holds b^2< a^2;
reserve T,T1,T2,S for non empty TopSpace;
theorem :: JGRAPH_2:9 :: BORSUK_2:1
for f being map of T1,S, g being map of T2,S,F1,F2 being Subset of T st
T1 is SubSpace of T & T2 is SubSpace of T & F1=[#] T1 & F2=[#] T2 &
([#] T1) \/ ([#] T2) = [#] T &
F1 is closed & F2 is closed &
f is continuous & g is continuous &
( for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p )
ex h being map of T,S st h = f+*g & h is continuous;
theorem :: JGRAPH_2:10
for n being Nat,q2 being Point of Euclid n,
q being Point of TOP-REAL n,
r being real number st q=q2 holds
Ball(q2,r) = {q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r};
theorem :: JGRAPH_2:11
(0.REAL 2)`1=0 & (0.REAL 2)`2=0;
theorem :: JGRAPH_2:12
1.REAL 2 = <* 1, 1 *>;
theorem :: JGRAPH_2:13
(1.REAL 2)`1=1 & (1.REAL 2)`2=1;
theorem :: JGRAPH_2:14
dom proj1=the carrier of TOP-REAL 2 & dom proj1=REAL 2;
theorem :: JGRAPH_2:15
dom proj2=the carrier of TOP-REAL 2 & dom proj2=REAL 2;
theorem :: JGRAPH_2:16
proj1 is map of TOP-REAL2,R^1;
theorem :: JGRAPH_2:17
proj2 is map of TOP-REAL2,R^1;
theorem :: JGRAPH_2:18
for p being Point of TOP-REAL 2 holds
p=|[proj1.p,proj2.p]|;
theorem :: JGRAPH_2:19
for B being Subset of TOP-REAL 2 st
B={0.REAL 2} holds B`<>{} & (the carrier of TOP-REAL 2)\B<>{};
theorem :: JGRAPH_2:20 :: BORSUK_1:def 2
for X,Y being non empty TopSpace,f being map of X,Y
holds f is continuous iff for p being Point of X,V being Subset of Y
st f.p in V & V is open holds
ex W being Subset of X st p in W & W is open & f.:W c= V;
theorem :: JGRAPH_2:21
for p being Point of TOP-REAL 2,
G being Subset of TOP-REAL 2
st G is open & p in G
ex r being real number st r>0 & {q where q is Point of TOP-REAL 2:
p`1-r<q`1 & q`1<p`1+r & p`2-r<q`2 & q`2<p`2+r} c= G;
theorem :: JGRAPH_2:22
for X,Y,Z being non empty TopSpace, B being Subset of Y,
C being Subset of Z,
f being map of X,Y, h being map of Y|B,Z|C
st f is continuous & h is continuous & rng f c= B & B<>{} & C<>{} holds
ex g being map of X,Z st g is continuous & g=h*f;
reserve p,q for Point of TOP-REAL 2;
definition
func Out_In_Sq -> Function of (the carrier of TOP-REAL 2)\{0.REAL 2},
(the carrier of TOP-REAL 2)\{0.REAL 2} means
:: JGRAPH_2:def 1
for p being Point of TOP-REAL 2 st p<>0.REAL 2 holds
((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies
it.p=|[1/p`1,p`2/p`1/p`1]|) &
(not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies
it.p=|[p`1/p`2/p`2,1/p`2]|);
end;
theorem :: JGRAPH_2:23
for p being Point of TOP-REAL 2 st
not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) holds
p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2;
theorem :: JGRAPH_2:24
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
Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|) &
(not (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies
Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]|);
theorem :: JGRAPH_2:25
for D being Subset of TOP-REAL 2,
K0 being Subset of (TOP-REAL 2)|D st
K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)
& p<>0.REAL 2} holds
rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0;
theorem :: JGRAPH_2:26
for D being Subset of TOP-REAL 2,
K0 being Subset of (TOP-REAL 2)|D st
K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)
& p<>0.REAL 2} holds
rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0;
theorem :: JGRAPH_2:27
for K0a being set,D being non empty Subset of TOP-REAL 2
st K0a={p where p is Point of TOP-REAL 2:
(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.REAL 2}
& D`={0.REAL 2}
holds K0a is non empty Subset of (TOP-REAL 2)|D &
K0a is non empty Subset of TOP-REAL 2;
theorem :: JGRAPH_2:28
for K0a being set,D being non empty Subset of TOP-REAL 2
st K0a={p where p is Point of TOP-REAL 2:
(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.REAL 2}
& D`={0.REAL 2}
holds K0a is non empty Subset of (TOP-REAL 2)|D &
K0a is non empty Subset of TOP-REAL 2;
theorem :: JGRAPH_2:29
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous &
f2 is continuous 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) & g is continuous;
theorem :: JGRAPH_2:30
for X being non empty TopSpace, a being real number holds
ex g being map of X,R^1 st (for p being Point of X holds g.p=a)
& g is continuous;
theorem :: JGRAPH_2:31
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous &
f2 is continuous 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) & g is continuous;
theorem :: JGRAPH_2:32
for X being non empty TopSpace, f1 being map of X,R^1 st f1 is continuous
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=r1*r1) & g is continuous;
theorem :: JGRAPH_2:33
for X being non empty TopSpace,
f1 being map of X,R^1,a being real number st f1 is continuous
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=a*r1) & g is continuous;
theorem :: JGRAPH_2:34
for X being non empty TopSpace,
f1 being map of X,R^1,a being real number st f1 is continuous
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=r1+a) & g is continuous;
theorem :: JGRAPH_2:35
for X being non empty TopSpace,
f1,f2 being map of X,R^1 st f1 is continuous &
f2 is continuous 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) & g is continuous;
theorem :: JGRAPH_2:36
for X being non empty TopSpace,
f1 being map of X,R^1 st f1 is continuous &
(for q being Point of X holds f1.q<>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=1/r1) & g is continuous;
theorem :: JGRAPH_2:37
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) & g is continuous;
theorem :: JGRAPH_2:38
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/r2) & g is continuous;
theorem :: JGRAPH_2:39
for K0 being Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K0,R^1 st
(for p being Point of (TOP-REAL 2)|K0 holds
f.p=proj1.p) holds f is continuous;
theorem :: JGRAPH_2:40
for K0 being Subset of TOP-REAL 2,
f being map of (TOP-REAL 2)|K0,R^1 st
(for p being Point of (TOP-REAL 2)|K0 holds
f.p=proj2.p) holds f is continuous;
theorem :: JGRAPH_2:41
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=1/p`1) & (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_2:42
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=1/p`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_2: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`2/p`1/p`1) & (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_2: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`1/p`2/p`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_2:45
for K0,B0 being Subset of TOP-REAL 2, f being map of
(TOP-REAL 2)|K0,(TOP-REAL 2)|B0,
f1,f2 being map of (TOP-REAL 2)|K0,R^1 st f1 is continuous &
f2 is continuous & K0<>{} & B0<>{} &
(for x,y,r,s being real number st |[x,y]| in K0 &
r=f1.(|[x,y]|) & s=f2.(|[x,y]|) holds
f.(|[x,y]|)=|[r,s]|) holds
f is continuous;
theorem :: JGRAPH_2:46
for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Out_In_Sq|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_2:47
for K0,B0 being Subset of TOP-REAL 2,f being
map of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0
st f=Out_In_Sq|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 TopSubset { P[set] } :
{ p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2;
scheme TopCompl { P[set], K() -> Subset of TOP-REAL 2 } :
K()` = { p where p is Point of TOP-REAL 2 : not P[p] }
provided
K() = { p where p is Point of TOP-REAL 2 : P[p] };
scheme ClosedSubset { F,G(Point of TOP-REAL 2) -> real number } :
{p where p is Point of TOP-REAL 2 : F(p) <= G(p) }
is closed Subset of TOP-REAL 2
provided
for p,q being Point of TOP-REAL 2 holds
F(p-q) = F(p) - F(q) & G(p-q) = G(p) - G(q) and
for p,q being Point of TOP-REAL 2 holds
(|. (p-q).|)^2 = (F(p-q))^2+(G(p-q))^2;
theorem :: JGRAPH_2:48
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=Out_In_Sq|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_2: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=Out_In_Sq|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_2:50
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=Out_In_Sq & h is continuous;
theorem :: JGRAPH_2:51
for B,K0,Kb being Subset of TOP-REAL 2 st B={0.REAL 2}
& K0={p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1}
& 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}
ex f being map of (TOP-REAL 2)|B`,(TOP-REAL 2)|B` st
f is continuous & f is one-to-one &
(for t being Point of TOP-REAL 2 st t in K0 & t<>0.REAL 2 holds
not f.t in K0 \/ Kb)
&(for r being Point of TOP-REAL 2 st not r in K0 \/ Kb holds f.r in K0)
&(for s being Point of TOP-REAL 2 st s in Kb holds f.s=s);
theorem :: JGRAPH_2:52
for f,g being map of I[01],TOP-REAL 2,
K0 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 &
K0={p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1}&
(f.O)`1=-1 & (f.I)`1=1 &
-1<=(f.O)`2 & (f.O)`2<=1 & -1<=(f.I)`2 & (f.I)`2<=1 &
(g.O)`2=-1 & (g.I)`2=1 &
-1<=(g.O)`1 & (g.O)`1<=1 & -1<=(g.I)`1 & (g.I)`1<=1 &
rng f misses K0 & rng g misses K0
holds rng f meets rng g;
theorem :: JGRAPH_2:53
for A,B,C,D being real number,
f being map of TOP-REAL 2,TOP-REAL 2
st (for t being Point of TOP-REAL 2 holds
f.t=|[A*(t`1)+B,C*(t`2)+D]|) holds f is continuous;
definition let A,B,C,D be real number;
func AffineMap(A,B,C,D) -> map of TOP-REAL 2,TOP-REAL 2 means
:: JGRAPH_2:def 2
for t being Point of TOP-REAL 2
holds it.t=|[A*(t`1)+B,C*(t`2)+D]|;
end;
definition let a,b,c,d be real number;
cluster AffineMap(a,b,c,d) -> continuous;
end;
theorem :: JGRAPH_2:54
for A,B,C,D being real number st A>0 & C>0
holds AffineMap(A,B,C,D) is one-to-one;
theorem :: JGRAPH_2:55
for f,g being map of I[01],TOP-REAL 2,a,b,c,d being real number,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
(f.O)`1=a & (f.I)`1=b &
c <=(f.O)`2 & (f.O)`2<=d & c <=(f.I)`2 & (f.I)`2<=d &
(g.O)`2=c & (g.I)`2=d &
a<=(g.O)`1 & (g.O)`1<=b & a<=(g.I)`1 & (g.I)`1<=b &
a < b & c < d &
not (ex r being Point of I[01] st
a<(f.r)`1 & (f.r)`1<b & c <(f.r)`2 & (f.r)`2<d)&
not (ex r being Point of I[01] st
a<(g.r)`1 & (g.r)`1<b & c <(g.r)`2 & (g.r)`2<d)
holds rng f meets rng g;
theorem :: JGRAPH_2:56
{p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 }
is closed Subset of TOP-REAL 2 &
{p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 }
is closed Subset of TOP-REAL 2;
theorem :: JGRAPH_2:57
{p7 where p7 is Point of TOP-REAL 2: -p7`1<=p7`2 }
is closed Subset of TOP-REAL 2 &
{p7 where p7 is Point of TOP-REAL 2: p7`2<=-p7`1 }
is closed Subset of TOP-REAL 2;
theorem :: JGRAPH_2:58
{p7 where p7 is Point of TOP-REAL 2: -p7`2<=p7`1 }
is closed Subset of TOP-REAL 2 &
{p7 where p7 is Point of TOP-REAL 2: p7`1<=-p7`2 }
is closed Subset of TOP-REAL 2;
Back to top