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;