:: On Outside Fashoda Meet Theorem :: by Yatsuka Nakamura :: :: Received July 16, 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, XBOOLE_0, PRE_TOPC, FUNCT_1, SUBSET_1, RCOMP_1, ORDINAL2, FUNCT_4, RELAT_1, STRUCT_0, TARSKI, EUCLID, METRIC_1, COMPLEX1, ARYTM_1, ARYTM_3, SUPINF_2, MCART_1, CARD_1, JORDAN2C, FINSEQ_1, REAL_1, XXREAL_0, PCOMPS_1, SQUARE_1, TOPMETR, XXREAL_1, FUNCOP_1, PARTFUN1, BORSUK_1, JGRAPH_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, FUNCOP_1, FINSEQ_1, FINSEQ_2, NAT_1, DOMAIN_1, STRUCT_0, PRE_TOPC, PCOMPS_1, TOPMETR, METRIC_1, RCOMP_1, SQUARE_1, PSCOMP_1, RLVECT_1, EUCLID, FUNCT_4; constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, MONOID_0, TOPMETR, PSCOMP_1, PCOMPS_1, FUNCOP_1, FUNCSDOM, FINSEQOP, MEASURE6, NUMBERS, COMSEQ_2; registrations RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, PRE_TOPC, BORSUK_1, MONOID_0, EUCLID, TOPMETR, PSCOMP_1, TOPS_1, ORDINAL1, VALUED_0, PARTFUN3; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve T,T1,T2,S for non empty TopSpace; theorem :: JGRAPH_2:1 :: BORSUK_2:1 for f being Function of T1,S, g being Function 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 object st p in ([#] T1) /\ ([#] T2) holds f.p = g.p ) ex h being Function of T,S st h = f+*g & h is continuous; theorem :: JGRAPH_2:2 for n being Element of NAT,q2 being Point of Euclid n, q being Point of TOP-REAL n, r being Real st q=q2 holds Ball(q2,r) = {q3 where q3 is Point of TOP-REAL n: |.q-q3.|; theorem :: JGRAPH_2:5 (1.REAL 2)`1=1 & (1.REAL 2)`2=1; theorem :: JGRAPH_2:6 dom proj1=the carrier of TOP-REAL 2 & dom proj1=REAL 2; theorem :: JGRAPH_2:7 dom proj2=the carrier of TOP-REAL 2 & dom proj2=REAL 2; theorem :: JGRAPH_2:8 for p being Point of TOP-REAL 2 holds p=|[proj1.p,proj2.p]|; theorem :: JGRAPH_2:9 for B being Subset of TOP-REAL 2 st B={0.TOP-REAL 2} holds B`<> {} & (the carrier of TOP-REAL 2)\B<>{}; theorem :: JGRAPH_2:10 :: BORSUK_1:def 2 for X,Y being non empty TopSpace,f being Function 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:11 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 st r>0 & {q where q is Point of TOP-REAL 2: p`1-r{} & C<>{} holds ex g being Function 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 NonZero TOP-REAL 2, NonZero TOP-REAL 2 means :: JGRAPH_2:def 1 for p being Point of TOP-REAL 2 st p<>0.TOP-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:13 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:14 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 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:15 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.TOP-REAL 2} holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0; theorem :: JGRAPH_2:16 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.TOP-REAL 2} holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0; theorem :: JGRAPH_2:17 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.TOP-REAL 2} & D`={0.TOP-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:18 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.TOP-REAL 2} & D`={0.TOP-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:19 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous 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 ) & g is continuous; theorem :: JGRAPH_2:20 for X being non empty TopSpace, a being Real holds ex g being Function of X,R^1 st (for p being Point of X holds g.p=a) & g is continuous; theorem :: JGRAPH_2:21 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous 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 ) & g is continuous; theorem :: JGRAPH_2:22 for X being non empty TopSpace, f1 being Function of X,R^1 st f1 is continuous 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=r1*r1) & g is continuous; theorem :: JGRAPH_2:23 for X being non empty TopSpace, f1 being Function of X,R^1,a being Real st f1 is continuous 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=a*r1) & g is continuous; theorem :: JGRAPH_2:24 for X being non empty TopSpace, f1 being Function of X,R^1,a being Real st f1 is continuous 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=r1+a) & g is continuous; theorem :: JGRAPH_2:25 for X being non empty TopSpace, f1,f2 being Function of X,R^1 st f1 is continuous & f2 is continuous 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 ) & g is continuous; theorem :: JGRAPH_2:26 for X being non empty TopSpace, f1 being Function of X,R^1 st f1 is continuous & (for q being Point of X holds f1.q<>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=1/r1) & g is continuous; theorem :: JGRAPH_2:27 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) & g is continuous; theorem :: JGRAPH_2:28 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/r2) & g is continuous; theorem :: JGRAPH_2:29 for K0 being Subset of TOP-REAL 2, f being Function 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:30 for K0 being Subset of TOP-REAL 2, f being Function 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:31 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=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:32 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=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: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`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: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`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:35 for K0,B0 being Subset of TOP-REAL 2, f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0, f1,f2 being Function of (TOP-REAL 2)|K0,R^1 st f1 is continuous & f2 is continuous & K0<>{} & B0<>{} & (for x,y,r,s being Real 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:36 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|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_2:37 for K0,B0 being Subset of TOP-REAL 2,f being Function of ( TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|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_2:sch 1 TopSubset { P[set] } : { p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2; scheme :: JGRAPH_2:sch 2 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 :: JGRAPH_2:sch 3 ClosedSubset { F,G(Point of TOP-REAL 2) -> Real } : {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:38 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=Out_In_Sq| 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_2: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=Out_In_Sq| 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_2:40 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=Out_In_Sq & h is continuous; theorem :: JGRAPH_2:41 for B,K0,Kb being Subset of TOP-REAL 2 st B={0.TOP-REAL 2} & K0= {p: -10.TOP-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:42 for f,g being Function 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 Function 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; registration let a,b,c,d be Real; cluster AffineMap(a,b,c,d) -> continuous; end; theorem :: JGRAPH_2:44 for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C ,D) is one-to-one; theorem :: JGRAPH_2:45 for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real , 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