The Mizar abstract of TOPREAL3

Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users
The abstract of the Mizar article:: Basic Properties of Connecting Points with Line Segments in $\calE^2_\rmT$
by
Yatsuka Nakamura, and
Jaroslaw Kotowicz
Received August 24, 1992
MML identifier: TOPREAL3
[ Mizar article, MML identifier index ]
environ

 vocabulary PRE_TOPC, EUCLID, FINSEQ_1, ARYTM, ARYTM_1, ARYTM_3, METRIC_1,
      RELAT_1, MCART_1, FUNCT_1, SQUARE_1, RVSUM_1, ABSVALUE, COMPLEX1,
      RLVECT_1, TOPREAL1, BOOLE, TARSKI, FINSEQ_2, FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, RELAT_1, FUNCT_1, STRUCT_0, FINSEQ_1, FUNCT_2, BINOP_1,
      PRE_TOPC, ABSVALUE, SQUARE_1, FINSEQ_2, FINSEQ_4, METRIC_1, FINSEQOP,
      RVSUM_1, EUCLID, TOPREAL1;
 constructors REAL_1, NAT_1, ABSVALUE, SQUARE_1, FINSEQOP, TOPREAL1, FINSEQ_4,
      INT_1, SEQ_1, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters FUNCT_1, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1, INT_1,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 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 number,
        u,u1,u2,u5 for Point of Euclid 2,
        n,m,i,j,k for Nat,
        x,y,z for set;

:::::::::::::::::::::::::::::
:: Real numbers preliminaries
:::::::::::::::::::::::::::::

canceled 2;

theorem :: TOPREAL3:3
r<s implies r < (r+s)/2 & (r+s)/2 < s;

begin
:::::::::::::::::::::::::::::::::::
:: Properties of sets in TOP-REAL 2
:::::::::::::::::::::::::::::::::::

canceled 2;

theorem :: TOPREAL3:6
1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*>;

theorem :: TOPREAL3:7
(p1+p2)`1 = p1`1 + p2`1 & (p1+p2)`2 = p1`2 + p2`2;

theorem :: TOPREAL3:8
  (p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2;

theorem :: TOPREAL3:9
(r*p)`1 = r*(p`1) & (r*p)`2 = r*(p`2);

theorem :: TOPREAL3:10
p1=<*r1,s1*> & p2=<*r2,s2*> implies p1+p2=<*r1+r2,s1+s2*> &
                                    p1-p2=<*r1-r2,s1-s2*>;

theorem :: TOPREAL3:11
p`1 = q`1 & p`2 = q`2 implies p=q;

theorem :: TOPREAL3:12
u1 = p1 & u2 = p2 implies
(Pitag_dist 2).(u1,u2) = sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2);

theorem :: TOPREAL3:13
the carrier of TOP-REAL n = the carrier of Euclid n;

 reserve r,r1,r2,lambda,s,s1,s2 for Real;

canceled;

theorem :: TOPREAL3:15
r1 < s1 implies {p1: p1`1=r & r1<=p1`2 & p1`2<=s1} = LSeg(|[r,r1]|,|[r,s1]|);

theorem :: TOPREAL3:16
r1 < s1 implies {p1: p1`2=r & r1<=p1 `1 & p1 `1<=s1} = LSeg(|[r1,r]|,|[s1,r]|);

theorem :: TOPREAL3:17
  p in LSeg(|[r,r1]|,|[r,s1]|) implies p`1 = r;

theorem :: TOPREAL3:18
  p in LSeg(|[r1,r]|,|[s1,r]|) implies p`2 = r;

theorem :: TOPREAL3:19
  p`1 <> q`1 & p`2 = q`2 implies |[(p`1+q`1)/2,p`2]| in LSeg(p,q);

theorem :: TOPREAL3:20
  p`1 = q`1 & p`2 <> q`2 implies |[p`1,(p`2+q`2)/2]| in LSeg(p,q);

theorem :: TOPREAL3:21
f = <* p,p1,q *> & i<>0 & j>i+1 implies LSeg(f,j) = {};

canceled;

theorem :: TOPREAL3:23
  f = <* p1,p2,p3 *> implies L~f = LSeg(p1,p2) \/ LSeg(p2,p3);

theorem :: TOPREAL3:24
i in dom f & j in dom(f|i) & j+1 in dom(f|i) implies LSeg(f,j) = LSeg(f|i,j);

theorem :: TOPREAL3:25
  j in dom f & j+1 in dom f implies LSeg(f^h,j) = LSeg(f,j);

theorem :: TOPREAL3:26
 for f being FinSequence of TOP-REAL n,i being Nat holds LSeg(f,i) c= L~f;

theorem :: TOPREAL3:27
  L~(f|i) c= L~f;

theorem :: TOPREAL3:28
for r being Real, 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:29
  u=p1 & p1=|[r1,s1]| & p2=|[r2,s2]| & p=|[r2,s1]| & p2 in Ball(u,r) implies
p in Ball(u,r);

theorem :: TOPREAL3:30
  |[s,r1]| in Ball(u,r) & |[s,s1]| in Ball(u,r) implies
|[s,(r1+s1)/2]| in Ball(u,r);

theorem :: TOPREAL3:31
   |[r1,s]| in Ball(u,r) & |[s1,s]| in Ball(u,r) implies
  |[(r1+s1)/2,s]| in Ball(u,r);

theorem :: TOPREAL3:32
  r1 <> s1 & s2 <> r2 & |[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:33
  not f/.1 in Ball(u,r) & 1<=m & m<=len f - 1 & LSeg(f,m) meets Ball(u,r) &
(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:34
  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:35
  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:36
 LSeg(p,|[p`1,q`2]|) /\ LSeg(|[p`1,q`2]|,q) ={|[p`1,q`2]|};

theorem :: TOPREAL3:37
LSeg(p,|[q`1,p`2]|) /\ LSeg(|[q`1,p`2]|,q) ={|[q`1,p`2]|};

theorem :: TOPREAL3:38
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:39
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:40
  i>2 & i in dom f & f is_S-Seq implies f|i is_S-Seq;

theorem :: TOPREAL3:41
  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_S-Seq;

theorem :: TOPREAL3:42
  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_S-Seq;

theorem :: TOPREAL3:43
  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_S-Seq;

theorem :: TOPREAL3:44
  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_S-Seq;

theorem :: TOPREAL3:45
  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:46
  len f>=2 & not p in L~f implies for n st 1<=n & n<=len f holds f/.n<>p;

theorem :: TOPREAL3:47
  q<>p & LSeg(q,p) /\ L~f = {q} implies not p in L~f;

theorem :: TOPREAL3:48
  f is_S-Seq & not f/.1 in Ball(u,r) & q in Ball(u,r) &
f/.len f in LSeg(f,m) & 1<=m & m + 1 <=len f & LSeg(f,m) meets Ball(u,r)
 implies m + 1 = len f;

theorem :: TOPREAL3:49
  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:50
  not p1 in Ball(u,r) & p in Ball(u,r) &
|[p`1,q`2]| in Ball(u,r) & q 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:51
  not p1 in Ball(u,r) & p in Ball(u,r) &
|[q`1,p`2]| in Ball(u,r) & q 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};
The abstract of the Mizar article:

Basic Properties of Connecting Points with Line Segments in $\calE^2_\rmT$
