:: Fashoda Meet Theorem for Rectangles :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received January 3, 2005 :: Copyright (c) 2005-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, PRE_TOPC, EUCLID, ARYTM_3, MCART_1, XXREAL_0, RLTOPSP1, ARYTM_1, REAL_1, CARD_1, RELAT_1, SUBSET_1, TOPREAL1, FUNCT_1, BORSUK_1, ORDINAL2, TOPS_2, JORDAN3, JGRAPH_6, PSCOMP_1, JORDAN17, JGRAPH_2, STRUCT_0, FUNCT_2, VALUED_1, TARSKI, XBOOLE_0; notations XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, TOPS_2, RLVECT_1, RLTOPSP1, EUCLID, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SUBSET_1, STRUCT_0, TOPMETR, PRE_TOPC, JORDAN6, JORDAN17, JGRAPH_2, XREAL_0, TOPREAL1, PSCOMP_1, REAL_1, JGRAPH_6, XXREAL_0; constructors REAL_1, RCOMP_1, TOPS_2, TOPMETR, TOPREAL1, SPPOL_2, PSCOMP_1, JORDAN6, JGRAPH_2, JORDAN17, JGRAPH_6, BINOP_2; registrations XBOOLE_0, RELSET_1, FUNCT_2, XREAL_0, MEMBERED, STRUCT_0, BORSUK_1, EUCLID, JGRAPH_2; requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM; begin theorem :: JGRAPH_7:1 for a,b,d being Real,p being Point of TOP-REAL 2 st a p3`1 & p4`2 <> p2`2 & p4`2 <=p1`2 & p1`2<=p2`2 & p1`1<=p2`1 & p2`1<=p3`1 & p4`2 <=p3`2 & p3 `2<=p2`2 & p1`1 =p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c holds p1,p2,p3,p4 are_in_this_order_on rectangle(a,b,c,d); theorem :: JGRAPH_7:31 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real st a=p2`2 & p2`2>p3`2 & p3`2>=c & a=p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c holds p1,p2,p3,p4 are_in_this_order_on rectangle(a,b,c,d); theorem :: JGRAPH_7:41 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real st a=p2`2 & p2`2>p3`2 & p3`2>= c & a =p1`2 & p1`2>p2 `2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c holds p1,p2,p3,p4 are_in_this_order_on rectangle(a,b,c,d); theorem :: JGRAPH_7:45 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real st a=p1`2 & p1`2>p2 `2 & p2`2>p3`2 & p3`2>= c & a=p1`2 & p1`2> p2`2 & p2`2>= c & b>=p3`1 & p3`1>p4`1 & p4`1>a holds p1,p2,p3,p4 are_in_this_order_on rectangle(a,b,c,d); theorem :: JGRAPH_7:47 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real st a=p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a holds p1,p2,p3,p4 are_in_this_order_on rectangle(a,b,c,d); theorem :: JGRAPH_7:48 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real st a=p1`1 & p1`1 >p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a holds p1,p2,p3,p4 are_in_this_order_on rectangle(a,b,c,d); theorem :: JGRAPH_7:49 for A,B,C,D being Real, h,g being Function of TOP-REAL 2, TOP-REAL 2 st A>0 & C>0 & h=AffineMap(A,B,C,D) & g=AffineMap(1/A,-B/A,1/C,-D/C) holds g=h" & h=g"; theorem :: JGRAPH_7:50 for A,B,C,D being Real, h being Function of TOP-REAL 2, TOP-REAL 2 st A>0 & C >0 & h=AffineMap(A,B,C,D) holds h is being_homeomorphism & for p1,p2 being Point of TOP-REAL 2 st p1`10 & C >0 & h=AffineMap(A,B,C,D) holds h is being_homeomorphism & for p1,p2 being Point of TOP-REAL 2 st p1`2=(f.O)`2 & (f. O)`2>(f.I)`2 & (f.I)`2>= c holds 1 >=((h*f).O)`2 & ((h*f).O)`2>((h*f).I)`2 & (( h*f).I)`2>= -1; theorem :: JGRAPH_7:66 for a,b,c,d being Real, h being Function of TOP-REAL 2, TOP-REAL 2,f being Function of I[01],TOP-REAL 2, O,I being Point of I[01] st a< b & c =p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4 `2>= c & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g; theorem :: JGRAPH_7:121 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real, P,Q being Subset of TOP-REAL 2 st a=p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c & P is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b ,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q; theorem :: JGRAPH_7:122 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real , f,g being Function of I[01],TOP-REAL 2 st a=p2`2 & p2`2>p3`2 & p3`2>= c & a < p4`1 & p4`1<=b & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g; theorem :: JGRAPH_7:123 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real, P,Q being Subset of TOP-REAL 2 st a=p2`2 & p2`2>p3`2 & p3`2>= c & a =p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c & f .0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g; theorem :: JGRAPH_7:129 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real, P,Q being Subset of TOP-REAL 2 st a=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>p4`2 & p4`2>= c & P is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q; theorem :: JGRAPH_7:130 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real , f,g being Function of I[01],TOP-REAL 2 st a=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>= c & a=p1`2 & p1`2>p2`2 & p2`2>p3`2 & p3`2>= c & a=p1`2 & p1`2>p2`2 & p2`2>= c & b>=p3`1 & p3`1>p4`1 & p4`1>a & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g; theorem :: JGRAPH_7:133 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real, P,Q being Subset of TOP-REAL 2 st a=p1`2 & p1`2>p2`2 & p2`2>= c & b>=p3`1 & p3`1>p4`1 & p4`1>a & P is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b ,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q; theorem :: JGRAPH_7:134 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real , f,g being Function of I[01],TOP-REAL 2 st a=p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g; theorem :: JGRAPH_7:135 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real, P,Q being Subset of TOP-REAL 2 st a=p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a & P is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b ,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q; theorem :: JGRAPH_7:136 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real , f,g being Function of I[01],TOP-REAL 2 st a=p1`1 & p1`1>p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & f is continuous one-to-one & g is continuous one-to-one & rng f c= closed_inside_of_rectangle(a,b,c,d) & rng g c= closed_inside_of_rectangle(a,b,c,d) holds rng f meets rng g; theorem :: JGRAPH_7:137 for p1,p2,p3,p4 being Point of TOP-REAL 2, a,b,c,d being Real, P,Q being Subset of TOP-REAL 2 st a=p1`1 & p1`1>p2`1 & p2`1>p3`1 & p3`1>p4`1 & p4`1> a & P is_an_arc_of p1,p3 & Q is_an_arc_of p2,p4 & P c= closed_inside_of_rectangle(a,b ,c,d) & Q c= closed_inside_of_rectangle(a,b,c,d) holds P meets Q;