:: The Topological Space ${\calE}^2_{\rm T}$. :: Arcs, Line Segments and Special Polygonal Arcs :: by Agata Darmochwa{\l} and Yatsuka Nakamura :: :: Received November 21, 1991 :: Copyright (c) 1991-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, REAL_1, NAT_1, XBOOLE_0, SUBSET_1, PRE_TOPC, EUCLID, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, CARD_1, STRUCT_0, XXREAL_1, RLTOPSP1, TARSKI, ARYTM_1, ARYTM_3, XXREAL_0, MCART_1, SUPINF_2, RCOMP_1, PCOMPS_1, CONNSP_2, TOPMETR, METRIC_1, TOPS_1, COMPLEX1, ORDINAL2, FINSEQ_1, PARTFUN1, ZFMISC_1, SETFAM_1, TOPREAL1; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, RCOMP_1, FINSEQ_1, FINSEQ_4, STRUCT_0, METRIC_1, TOPMETR, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, PRE_TOPC, XXREAL_0; constructors SETFAM_1, REAL_1, NAT_1, COMPLEX1, FINSEQOP, RCOMP_1, FINSEQ_4, TOPS_1, TOPS_2, COMPTS_1, EUCLID, TOPMETR, RVSUM_1, VALUED_1, FUNCSDOM, RLTOPSP1, CONVEX1, BINOP_2, PCOMPS_1, RUSUB_4; registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, EUCLID, TOPMETR, VALUED_0, RLTOPSP1, FUNCT_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve r,lambda for Real, i,j,n for Nat; :: PRELIMINARIES scheme :: TOPREAL1:sch 1 FraenkelAlt {A() -> non empty set, P[set], Q[set]}: {v where v is Element of A(): P[v] or Q[v]} = {v1 where v1 is Element of A(): P[v1]} \/ {v2 where v2 is Element of A(): Q[v2]}; :: PROPER TEXT reserve p,p1,p2,q1,q2 for Point of TOP-REAL 2, P, P1 for Subset of TOP-REAL 2; reserve T for TopSpace; definition let T; let p1, p2 be Point of T, P be Subset of T; pred P is_an_arc_of p1,p2 means :: TOPREAL1:def 1 ex f being Function of I[01], T|P st f is being_homeomorphism & f.0 = p1 & f.1 = p2; end; theorem :: TOPREAL1:1 for P being Subset of T, p1,p2 being Point of T st P is_an_arc_of p1,p2 holds p1 in P & p2 in P; theorem :: TOPREAL1:2 for T being T_2 TopSpace for P,Q being Subset of T, p1,p2,q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds P \/ Q is_an_arc_of p1,q1; definition func R^2-unit_square -> Subset of TOP-REAL 2 equals :: TOPREAL1:def 2 ( LSeg(|[0,0]|,|[0,1]|) \/ LSeg(|[0,1]|,|[1,1]|) ) \/ ( LSeg(|[1,1]|,|[1,0]|) \/ LSeg(|[1,0]|,|[0,0]|) ); end; theorem :: TOPREAL1:3 p1`1 <= p2`1 & p in LSeg(p1,p2) implies p1`1 <= p`1 & p`1 <= p2`1; theorem :: TOPREAL1:4 p1`2 <= p2`2 & p in LSeg(p1,p2) implies p1`2 <= p`2 & p`2 <= p2`2; theorem :: TOPREAL1:5 for p,p1,p2 being Point of TOP-REAL n st p in LSeg(p1,p2) holds LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2); theorem :: TOPREAL1:6 for p1,p2,q1,q2 being Point of TOP-REAL n st q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) holds LSeg(q1,q2) c= LSeg(p1,p2); theorem :: TOPREAL1:7 for p,q,p1,p2 being Point of TOP-REAL n st p in LSeg(p1,p2) & q in LSeg(p1,p2) holds LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,q) \/ LSeg(q,p2); theorem :: TOPREAL1:8 for p, p1, p2 being Point of TOP-REAL n st p in LSeg(p1,p2) holds LSeg (p1,p) /\ LSeg(p,p2) = {p}; registration let n; cluster the carrier of TOP-REAL n -> functional; end; theorem :: TOPREAL1:9 for p1,p2 being Point of TOP-REAL n st p1 <> p2 holds LSeg(p1,p2) is_an_arc_of p1,p2; registration let n; cluster TOP-REAL n -> T_2; end; theorem :: TOPREAL1:10 for P being Subset of TOP-REAL n, p1,p2,q1 being Point of TOP-REAL n st P is_an_arc_of p1,p2 & P /\ LSeg(p2,q1) = {p2} holds P \/ LSeg(p2 ,q1) is_an_arc_of p1,q1; theorem :: TOPREAL1:11 for P being Subset of TOP-REAL n, p1,p2,q1 being Point of TOP-REAL n st P is_an_arc_of p2,p1 & LSeg(q1,p2) /\ P = {p2} holds LSeg(q1,p2) \/ P is_an_arc_of q1,p1; theorem :: TOPREAL1:12 for p1,p2,q1 being Point of TOP-REAL n st (p1 <> p2 or p2 <> q1) & LSeg(p1,p2) /\ LSeg(p2,q1) = {p2} holds LSeg(p1,p2) \/ LSeg(p2,q1) is_an_arc_of p1,q1; theorem :: TOPREAL1:13 LSeg(|[ 0,0 ]|, |[ 0,1 ]|) = { p1 : p1`1 = 0 & p1`2 <= 1 & p1`2 >= 0} & LSeg(|[ 0,1 ]|, |[ 1,1 ]|) = { p2 : p2`1 <= 1 & p2`1 >= 0 & p2`2 = 1} & LSeg(|[ 0,0 ]|, |[ 1,0 ]|) = { q1 : q1`1 <= 1 & q1`1 >= 0 & q1`2 = 0} & LSeg(|[ 1,0 ]|, |[ 1,1 ]|) = { q2 : q2`1 = 1 & q2`2 <= 1 & q2`2 >= 0}; theorem :: TOPREAL1:14 R^2-unit_square ={ p : p`1 = 0 & p`2 <= 1 & p`2 >= 0 or p`1 <= 1 & p`1 >= 0 & p`2 = 1 or p`1 <= 1 & p`1 >= 0 & p`2 = 0 or p`1 = 1 & p`2 <= 1 & p`2 >= 0}; registration cluster R^2-unit_square -> non empty; end; theorem :: TOPREAL1:15 LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,1]|,|[1,1]|) = {|[0,1]|}; theorem :: TOPREAL1:16 LSeg(|[0,0]|,|[1,0]|) /\ LSeg(|[1,0]|,|[1,1]|) = {|[1,0]|}; theorem :: TOPREAL1:17 LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,0]|,|[1,0]|) = {|[0,0]|}; theorem :: TOPREAL1:18 LSeg(|[0,1]|,|[1,1]|) /\ LSeg(|[1,0]|,|[1,1]|) = {|[1,1]|}; theorem :: TOPREAL1:19 LSeg(|[0,0]|,|[1,0]|) misses LSeg(|[0,1]|,|[1,1]|); theorem :: TOPREAL1:20 LSeg(|[0,0]|,|[0,1]|) misses LSeg(|[1,0]|,|[1,1]|); definition let n; let f be FinSequence of TOP-REAL n; let i; func LSeg(f,i) -> Subset of TOP-REAL n equals :: TOPREAL1:def 3 LSeg(f/.i,f/.(i+1)) if 1 <= i & i+1 <= len f otherwise {}; end; theorem :: TOPREAL1:21 for f being FinSequence of TOP-REAL n st 1 <= i & i+1 <= len f holds f/.i in LSeg(f,i) & f/.(i+1) in LSeg(f,i); definition let n; let f be FinSequence of TOP-REAL n; func L~f -> Subset of TOP-REAL n equals :: TOPREAL1:def 4 union { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f }; end; theorem :: TOPREAL1:22 for f being FinSequence of TOP-REAL n holds len f = 0 or len f = 1 iff L~f = {}; theorem :: TOPREAL1:23 for f being FinSequence of TOP-REAL n holds len f >= 2 implies L~f <> {}; definition let IT be FinSequence of TOP-REAL 2; attr IT is special means :: TOPREAL1:def 5 for i st 1 <= i & i+1 <= len IT holds (IT/.i)`1 = ( IT/.(i+1))`1 or (IT/.i)`2 = (IT/.(i+1))`2; attr IT is unfolded means :: TOPREAL1:def 6 for i st 1 <= i & i + 2 <= len IT holds LSeg(IT,i) /\ LSeg(IT,i+1) = {IT/.(i+1)}; attr IT is s.n.c. means :: TOPREAL1:def 7 for i,j st i+1 < j holds LSeg(IT,i) misses LSeg(IT,j); end; reserve f,f1,f2,h for FinSequence of TOP-REAL 2; definition let f; attr f is being_S-Seq means :: TOPREAL1:def 8 f is one-to-one & len f >= 2 & f is unfolded s.n.c. special; end; theorem :: TOPREAL1:24 ex f1,f2 st f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = L~f1 \/ L~f2 & L~f1 /\ L~f2 = {|[ 0,0 ]|, |[ 1,1 ]|} & f1/.1 = |[0,0]| & f1/.len f1=|[1,1]| & f2/.1 = |[0,0]| & f2/.len f2 = |[1,1]|; theorem :: TOPREAL1:25 h is being_S-Seq implies L~h is_an_arc_of h/.1,h/.len h; definition let P be Subset of TOP-REAL 2; attr P is being_S-P_arc means :: TOPREAL1:def 9 ex f st f is being_S-Seq & P = L~f; end; theorem :: TOPREAL1:26 P1 is being_S-P_arc implies P1 <> {}; registration cluster being_S-P_arc -> non empty for Subset of TOP-REAL 2; end; theorem :: TOPREAL1:27 ex P1, P2 being non empty Subset of TOP-REAL 2 st P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[ 0,0 ]|, |[ 1,1 ]|}; theorem :: TOPREAL1:28 P is being_S-P_arc implies ex p1,p2 st P is_an_arc_of p1,p2; theorem :: TOPREAL1:29 P is being_S-P_arc implies ex f being Function of I[01], (TOP-REAL 2)| P st f is being_homeomorphism; :: Moved from JORDAN1A, AK, 23.02.2006 scheme :: TOPREAL1:sch 2 TRSubsetEx { n() -> Nat, P[object] } : ex A being Subset of TOP-REAL n() st for p being Point of TOP-REAL n() holds p in A iff P[p]; scheme :: TOPREAL1:sch 3 TRSubsetUniq { n() -> Nat, P[object] } : for A, B being Subset of TOP-REAL n() st (for p being Point of TOP-REAL n() holds p in A iff P[p]) & (for p being Point of TOP-REAL n() holds p in B iff P[p]) holds A = B; definition let p be Point of TOP-REAL 2; func north_halfline p -> Subset of TOP-REAL 2 means :: TOPREAL1:def 10 for x being Point of TOP-REAL 2 holds x in it iff x`1 = p`1 & x`2 >= p`2; func east_halfline p -> Subset of TOP-REAL 2 means :: TOPREAL1:def 11 for x being Point of TOP-REAL 2 holds x in it iff x`1 >= p`1 & x`2 = p`2; func south_halfline p -> Subset of TOP-REAL 2 means :: TOPREAL1:def 12 for x being Point of TOP-REAL 2 holds x in it iff x`1 = p`1 & x`2 <= p`2; func west_halfline p -> Subset of TOP-REAL 2 means :: TOPREAL1:def 13 for x being Point of TOP-REAL 2 holds x in it iff x`1 <= p`1 & x`2 = p`2; end; theorem :: TOPREAL1:30 north_halfline p = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 >= p`2} ; theorem :: TOPREAL1:31 north_halfline p = { |[ p`1,r ]| where r is Real: r >= p`2 }; theorem :: TOPREAL1:32 east_halfline p = {q where q is Point of TOP-REAL 2: q`1 >= p`1 & q`2 = p`2}; theorem :: TOPREAL1:33 east_halfline p = { |[ r,p`2 ]| where r is Real: r >= p`1 }; theorem :: TOPREAL1:34 south_halfline p = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 <= p`2} ; theorem :: TOPREAL1:35 south_halfline p = { |[ p`1,r ]| where r is Real: r <= p`2 }; theorem :: TOPREAL1:36 west_halfline p = {q where q is Point of TOP-REAL 2: q`1 <= p`1 & q`2 = p`2}; theorem :: TOPREAL1:37 west_halfline p = { |[ r,p`2 ]| where r is Real: r <= p`1 }; registration let p be Point of TOP-REAL 2; cluster north_halfline p -> non empty; cluster east_halfline p -> non empty; cluster south_halfline p -> non empty; cluster west_halfline p -> non empty; end; :: Moved from JORDAN1C, AK, 23.02.2006 theorem :: TOPREAL1:38 p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p;