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

The abstract of the Mizar article:

On Outside Fashoda Meet Theorem

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