:: Basic Properties of Connecting Points with Line Segments :: in ${\calE}^2_{\rm T}$ :: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz :: :: Received August 24, 1992 :: Copyright (c) 1992-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, FINSEQ_1, SUBSET_1, RELAT_1, ARYTM_3, MCART_1, ARYTM_1, FUNCT_1, SQUARE_1, BINOP_2, COMPLEX1, RVSUM_1, CARD_3, NAT_1, STRUCT_0, REAL_1, XXREAL_0, RLTOPSP1, TARSKI, CARD_1, XBOOLE_0, TOPREAL1, PARTFUN1, ORDINAL4, METRIC_1, FINSEQ_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, BINOP_1, PRE_TOPC, FINSEQ_2, STRUCT_0, METRIC_1, RVSUM_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, XXREAL_0; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, FINSEQ_4, TOPREAL1, RVSUM_1, RELSET_1, DOMAIN_1, BINOP_1; registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, VALUED_0, INT_1, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve p,p1,p2,p3,p11,p22,q,q1,q2 for Point of TOP-REAL 2, f,h for FinSequence of TOP-REAL 2, r,r1,r2,s,s1,s2 for Real, u,u1,u2,u5 for Point of Euclid 2, n,m,i,j,k for Nat, N for Nat, x,y,z for set; begin :: Properties of sets in TOP-REAL 2 ::$CT theorem :: TOPREAL3:2 (p1+p2)`1 = p1`1 + p2`1 & (p1+p2)`2 = p1`2 + p2`2; theorem :: TOPREAL3:3 (p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2; theorem :: TOPREAL3:4 (r*p)`1 = r*(p`1) & (r*p)`2 = r*(p`2); theorem :: TOPREAL3:5 p1=<*r1,s1*> & p2=<*r2,s2*> implies p1+p2=<*r1+r2,s1+s2*> & p1- p2=<*r1-r2,s1-s2*>; theorem :: TOPREAL3:6 p`1 = q`1 & p`2 = q`2 implies p=q; theorem :: TOPREAL3:7 u1 = p1 & u2 = p2 implies (Pitag_dist 2).(u1,u2) = sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2); theorem :: TOPREAL3:8 for n being Nat holds the carrier of TOP-REAL n = the carrier of Euclid n; reserve lambda for Real; theorem :: TOPREAL3:9 r1 <= s1 implies {p1: p1`1=r & r1<=p1`2 & p1`2<=s1} = LSeg(|[r, r1]|,|[r,s1]|); theorem :: TOPREAL3:10 r1 <= s1 implies {p1: p1`2=r & r1<=p1`1 & p1`1<=s1} = LSeg(|[r1, r]|,|[s1,r]|); theorem :: TOPREAL3:11 p in LSeg(|[r,r1]|,|[r,s1]|) implies p`1 = r; theorem :: TOPREAL3:12 p in LSeg(|[r1,r]|,|[s1,r]|) implies p`2 = r; theorem :: TOPREAL3:13 p`1 <> q`1 & p`2 = q`2 implies |[(p`1+q`1)/2,p`2]| in LSeg(p,q); theorem :: TOPREAL3:14 p`1 = q`1 & p`2 <> q`2 implies |[p`1,(p`2+q`2)/2]| in LSeg(p,q); theorem :: TOPREAL3:15 for i,j be Nat holds f = <* p,p1,q *> & i<>0 & j>i+1 implies LSeg(f,j) = {}; theorem :: TOPREAL3:16 f = <* p1,p2,p3 *> implies L~f = LSeg(p1,p2) \/ LSeg(p2,p3); theorem :: TOPREAL3:17 j in dom(f|i) & j+1 in dom(f|i) implies LSeg(f,j) = LSeg(f|i,j); theorem :: TOPREAL3:18 j in dom f & j+1 in dom f implies LSeg(f^h,j) = LSeg(f,j); theorem :: TOPREAL3:19 for f being FinSequence of TOP-REAL n,i being Nat holds LSeg(f,i ) c= L~f; theorem :: TOPREAL3:20 L~(f|i) c= L~f; theorem :: TOPREAL3:21 for p1,p2 being Point of TOP-REAL N, u being Point of Euclid N st p1 in Ball(u,r) & p2 in Ball(u,r) holds LSeg(p1,p2) c= Ball(u,r); theorem :: TOPREAL3:22 u=p1 & p1=|[r1,s1]| & p2=|[r2,s2]| & p=|[r2,s1]| & p2 in Ball(u,r) implies p in Ball(u,r); theorem :: TOPREAL3:23 |[s,r1]| in Ball(u,r) & |[s,s1]| in Ball(u,r) implies |[s,(r1+s1)/2]| in Ball(u,r); theorem :: TOPREAL3:24 |[r1,s]| in Ball(u,r) & |[s1,s]| in Ball(u,r) implies |[(r1+s1)/2,s]| in Ball(u,r); theorem :: TOPREAL3:25 |[r1,r2]| in Ball(u,r) & |[s1,s2]| in Ball(u,r) implies |[r1,s2]| in Ball(u,r) or |[s1,r2]| in Ball(u,r); theorem :: TOPREAL3:26 not f/.1 in Ball(u,r) & 1<=m & m<=len f - 1 & (for i st 1<=i & i<=len f - 1 & LSeg(f,i) /\ Ball(u,r) <> {} holds m<=i) implies not f/.m in Ball(u,r); theorem :: TOPREAL3:27 for q,p2,p st q`2 = p2`2 & p`2 <> p2`2 holds (LSeg(p2,|[p2`1,p`2]|) \/ LSeg(|[p2`1,p`2]|,p)) /\ LSeg(q,p2) = {p2}; theorem :: TOPREAL3:28 for q,p2,p st q`1 = p2`1 & p`1 <> p2`1 holds (LSeg(p2,|[p`1,p2`2]|) \/ LSeg(|[p`1,p2`2]|,p)) /\ LSeg(q,p2) = {p2}; theorem :: TOPREAL3:29 LSeg(p,|[p`1,q`2]|) /\ LSeg(|[p`1,q`2]|,q) ={|[p`1,q`2]|}; theorem :: TOPREAL3:30 LSeg(p,|[q`1,p`2]|) /\ LSeg(|[q`1,p`2]|,q) ={|[q`1,p`2]|}; theorem :: TOPREAL3:31 p`1 = q`1 & p`2 <> q`2 implies LSeg(p,|[p`1,(p`2+q`2)/2]|) /\ LSeg(|[p`1,(p`2+q`2)/2]|,q)={|[p`1,(p`2+q`2)/2]|}; theorem :: TOPREAL3:32 p`1 <> q`1 & p`2 = q`2 implies LSeg(p,|[(p`1+q`1)/2,p`2]|) /\ LSeg(|[(p`1+q`1)/2,p`2]|,q)={|[(p`1+q`1)/2,p`2]|}; theorem :: TOPREAL3:33 i>2 & i in dom f & f is being_S-Seq implies f|i is being_S-Seq; theorem :: TOPREAL3:34 p`1 <> q`1 & p`2 <> q`2 & f = <* p,|[p`1,q`2]|,q *> implies f/.1 = p & f/.len f = q & f is being_S-Seq; theorem :: TOPREAL3:35 p`1 <> q`1 & p`2 <> q`2 & f = <* p,|[q`1,p`2]|,q *> implies f/.1 = p & f/.len f = q & f is being_S-Seq; theorem :: TOPREAL3:36 p`1 = q`1 & p`2 <> q`2 & f = <* p,|[p`1,(p`2 + q`2)/2]|,q *> implies f /.1 = p & f/.len f = q & f is being_S-Seq; theorem :: TOPREAL3:37 p`1 <> q`1 & p`2 = q`2 & f = <* p,|[(p`1 + q`1)/2,p`2]|,q *> implies f /.1 = p & f/.len f = q & f is being_S-Seq; theorem :: TOPREAL3:38 i in dom f & i+1 in dom f implies L~(f| (i+1)) = L~(f|i) \/ LSeg(f/.i,f /.(i+1)); theorem :: TOPREAL3:39 len f>=2 & not p in L~f implies for n st 1<=n & n<=len f holds f/.n<>p; theorem :: TOPREAL3:40 q<>p & LSeg(q,p) /\ L~f = {q} implies not p in L~f; theorem :: TOPREAL3:41 f is being_S-Seq & f/.len f in LSeg(f,m) & 1<=m & m + 1 <=len f implies m + 1 = len f; theorem :: TOPREAL3:42 not p1 in Ball(u,r) & q in Ball(u,r) & p in Ball(u,r) & not p in LSeg( p1,q ) & ( q`1=p`1 & q`2<>p`2 or q`1<>p`1 & q`2=p`2 ) & (p1`1=q`1 or p1`2=q`2) implies LSeg(p1,q) /\ LSeg(q,p) = {q}; theorem :: TOPREAL3:43 not p1 in Ball(u,r) & p in Ball(u,r) & |[p`1,q`2]| in Ball(u,r) & not |[p`1,q`2]| in LSeg(p1,p) & p1`1 = p`1 & p`1<>q`1 & p`2<>q`2 implies (LSeg(p,|[ p`1,q`2]|) \/ LSeg(|[p`1,q`2]|,q)) /\ LSeg(p1,p) = {p}; theorem :: TOPREAL3:44 not p1 in Ball(u,r) & p in Ball(u,r) & |[q`1,p`2]| in Ball(u,r) & not |[q`1,p`2]| in LSeg(p1,p) & p1`2 = p`2 & p`1<>q`1 & p`2<>q`2 implies (LSeg(p,|[ q`1,p`2]|) \/ LSeg(|[q`1,p`2]|,q)) /\ LSeg(p1,p) = {p}; reserve f for FinSequence of REAL; theorem :: TOPREAL3:45 len f = n implies f in the carrier of Euclid n; theorem :: TOPREAL3:46 len f = n implies f in the carrier of TOP-REAL n;