:: Extremal Properties of Vertices on Special Polygons I
::  by Yatsuka Nakamura and Czes\law Byli\'nski
::
:: Received May 11, 1994
:: Copyright (c) 1994-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, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FINSEQ_1,
      XBOOLE_0, RELAT_1, FINSET_1, TARSKI, COMPLEX1, REAL_1, PRE_TOPC, EUCLID,
      METRIC_1, FUNCT_1, RCOMP_1, RLTOPSP1, CARD_1, SEQ_4, XXREAL_2, PCOMPS_1,
      STRUCT_0, SUPINF_2, TEX_2, COMPTS_1, TOPREAL1, BORSUK_1, TOPS_2,
      ORDINAL2, MCART_1, ZFMISC_1, PARTFUN1, SETFAM_1, SPPOL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0,
      XXREAL_2, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, SEQ_4, FUNCT_1,
      BINOP_1, PARTFUN1, PRE_TOPC, BORSUK_1, FINSET_1, FINSEQ_1, FINSEQ_4,
      DOMAIN_1, STRUCT_0, METRIC_1, PCOMPS_1, TOPS_2, ZFMISC_1, COMPTS_1,
      RLVECT_1, RLTOPSP1, EUCLID, TEX_2, TOPREAL1;
 constructors SETFAM_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, FINSEQ_4,
      TOPS_2, COMPTS_1, REALSET2, TDLAT_3, TEX_2, MONOID_0, TOPMETR, TOPREAL1,
      PCOMPS_1, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0,
      INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TEX_2, EUCLID, TOPREAL1,
      FINSET_1, VALUED_0, RLTOPSP1, FUNCT_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaires

reserve n,i,k,m for Nat;

theorem :: SPPOL_1:1
  for n,k being Nat holds n<k implies n<=k-1;

theorem :: SPPOL_1:2
  1<=k-m & k-m<=n implies k-m in Seg n & k-m is Element of NAT;

scheme :: SPPOL_1:sch 1
  FinSeqFam{D()-> non empty set,f()->FinSequence of D(), F(FinSequence of D(),
  Nat)->set,P[Nat]}:
 {F(f(),i): i in dom f() & P[i]} is finite;

scheme :: SPPOL_1:sch 2
  FinSeqFam9{D()-> non empty set,f()-> FinSequence of D(), F(FinSequence of D(
),Nat)->set,P[set]}:
{F(f(),i): 1<=i & i<=len f() & P[i]} is finite;

theorem :: SPPOL_1:3
  for x1,x2,x3 being Element of REAL n holds |.x1 - x2.|- |.x2 -
  x3.| <= |.x1 - x3.|;

theorem :: SPPOL_1:4
  for x1,x2,x3 being Element of REAL n holds |.x2 - x1.|- |.x2 - x3.| <=
  |.x3 - x1.|;

begin

:: Extremal properties of endpoints of line segments in n-dimensional
:: Euclidean space

reserve r,r1,r2,s,s1,s2 for Real;
reserve p,p1,p2,q1,q2 for Point of TOP-REAL n;

theorem :: SPPOL_1:5
  for u1,u2 being Point of Euclid n, v1,v2 being Element of REAL n
  st v1=u1 & v2=u2 holds dist(u1,u2) = |.v1-v2.|;

theorem :: SPPOL_1:6
  for P being non empty Subset of TOP-REAL n st P is closed & P c= LSeg(
  p1,p2) ex s st (1-s)*p1+s*p2 in P & for r st 0<=r & r<=1 & (1-r)*p1+r*p2 in P
  holds s<=r;

theorem :: SPPOL_1:7
  for p1,p2,q1,q2 st LSeg(q1,q2) c= LSeg(p1,p2) & p1 in LSeg(q1,q2
  ) holds p1=q1 or p1=q2;

theorem :: SPPOL_1:8
  for p1,p2,q1,q2 st LSeg(p1,p2) = LSeg(q1,q2) holds p1=q1 & p2=q2 or p1
  =q2 & p2=q1;

registration
  let n,p1,p2;
  cluster LSeg(p1,p2) -> compact;
 cluster LSeg(p1,p2) -> closed;
end;

definition
  let n,p;
  let P be Subset of TOP-REAL n;
  pred p is_extremal_in P means
:: SPPOL_1:def 1

  p in P & for p1,p2 st p in LSeg(p1,p2) & LSeg(p1,p2) c= P holds p=p1 or p=p2;
end;

theorem :: SPPOL_1:9
  for P,Q being Subset of TOP-REAL n st p is_extremal_in P & Q c= P & p
  in Q holds p is_extremal_in Q;

theorem :: SPPOL_1:10
  p is_extremal_in {p};

theorem :: SPPOL_1:11
  p1 is_extremal_in LSeg(p1,p2);

theorem :: SPPOL_1:12
  p2 is_extremal_in LSeg(p1,p2);

theorem :: SPPOL_1:13
  p is_extremal_in LSeg(p1,p2) implies p = p1 or p = p2;

begin

:: Extremal properties of vertices of special polygons

reserve P,Q for Subset of TOP-REAL 2,
  f,f1,f2 for FinSequence of the carrier of TOP-REAL 2,
  p,p1,p2,p3,q,q3 for Point of TOP-REAL 2;

theorem :: SPPOL_1:14
  for p1,p2 st p1`1<>p2`1 & p1`2<>p2`2 ex p st p in LSeg(p1,p2) &
  p`1<>p1`1 & p`1<>p2`1 & p`2<>p1`2 & p`2<>p2`2;

definition
  let P;
  attr P is horizontal means
:: SPPOL_1:def 2

  for p,q st p in P & q in P holds p`2=q`2;
  attr P is vertical means
:: SPPOL_1:def 3

  for p,q st p in P & q in P holds p`1=q`1;
end;

registration
  cluster non trivial horizontal -> non vertical for Subset of TOP-REAL 2;
  cluster non trivial vertical -> non horizontal for Subset of TOP-REAL 2;
end;

theorem :: SPPOL_1:15
  p`2=q`2 iff LSeg(p,q) is horizontal;

theorem :: SPPOL_1:16
  p`1=q`1 iff LSeg(p,q) is vertical;

theorem :: SPPOL_1:17
  p1 in LSeg(p,q) & p2 in LSeg(p,q) & p1`1<>p2`1 & p1`2=p2`2 implies
  LSeg(p,q) is horizontal;

theorem :: SPPOL_1:18
  p1 in LSeg(p,q) & p2 in LSeg(p,q) & p1`2<>p2`2 & p1`1=p2`1 implies
  LSeg(p,q) is vertical;

registration
  let f,i;
  cluster LSeg(f,i) -> closed;
end;

theorem :: SPPOL_1:19
  f is special implies LSeg(f,i) is vertical or LSeg(f,i) is horizontal;

theorem :: SPPOL_1:20
  f is one-to-one & 1 <= i & i+1 <= len f implies LSeg(f,i) is non trivial;

theorem :: SPPOL_1:21
  f is one-to-one & 1 <= i & i+1 <= len f & LSeg(f,i) is vertical
  implies LSeg(f,i) is non horizontal;

theorem :: SPPOL_1:22
  for f holds {LSeg(f,i): 1<=i & i<=len f} is finite;

theorem :: SPPOL_1:23
  for f holds {LSeg(f,i): 1<=i & i+1<=len f}
     is finite;

theorem :: SPPOL_1:24
  for f holds {LSeg(f,i): 1<=i & i<=len f} is Subset-Family of TOP-REAL 2;

theorem :: SPPOL_1:25
  for f holds {LSeg(f,i): 1<=i & i+1<=len f} is Subset-Family of TOP-REAL 2;

theorem :: SPPOL_1:26
  for f st Q = union{LSeg(f,i): 1<=i & i+1<=len f} holds Q is closed;

registration
  let f;
  cluster L~f -> closed;
end;

definition
  let IT be FinSequence of TOP-REAL 2;
  attr IT is alternating means
:: SPPOL_1:def 4

  for i st 1 <= i & i+2 <= len IT holds (
  IT/.i)`1 <> (IT/.(i+2))`1 & (IT/.i)`2 <> (IT/.(i+2))`2;
end;

theorem :: SPPOL_1:27
  f is special alternating & 1 <= i & i+2 <= len f & (f/.i)`1 = (f
  /.(i+1))`1 implies (f/.(i+1))`2 = (f/.(i+2))`2;

theorem :: SPPOL_1:28
  f is special alternating & 1 <= i & i+2 <= len f & (f/.i)`2 = (f
  /.(i+1))`2 implies (f/.(i+1))`1 = (f/.(i+2))`1;

theorem :: SPPOL_1:29
  f is special alternating & 1 <= i & i+2 <= len f & p1 = f/.i &
p2 = f/.(i+1) & p3 = f/.(i+2) implies p1`1 = p2`1 & p3`1 <> p2`1 or p1`2 = p2`2
  & p3`2 <> p2`2;

theorem :: SPPOL_1:30
  f is special alternating & 1 <= i & i+2 <= len f & p1 = f/.i & p2 = f
/.(i+1) & p3 = f/.(i+2) implies p2`1 = p3`1 & p1`1 <> p2`1 or p2`2 = p3`2 & p1
  `2 <> p2`2;

theorem :: SPPOL_1:31
  f is special alternating & 1<=i & i+2<=len f implies not LSeg(f/.i,f/.
  (i+2)) c= LSeg(f,i) \/ LSeg(f,i+1);

theorem :: SPPOL_1:32
  f is special alternating & 1<=i & i+2<=len f & LSeg(f,i) is
  vertical implies LSeg(f,i+1) is horizontal;

theorem :: SPPOL_1:33
  f is special alternating & 1<=i & i+2<=len f & LSeg(f,i) is
  horizontal implies LSeg(f,i+1) is vertical;

theorem :: SPPOL_1:34
  f is special alternating & 1<=i & i+2<=len f implies LSeg(f,i) is
  vertical & LSeg(f,i+1) is horizontal or LSeg(f,i) is horizontal & LSeg(f,i+1)
  is vertical;

theorem :: SPPOL_1:35
  f is special alternating & 1<=i & i+2<=len f & f/.(i+1) in LSeg(
  p,q) & LSeg(p,q) c= LSeg(f,i) \/ LSeg(f,i+1) implies f/.(i+1)=p or f/.(i+1)=q
;

theorem :: SPPOL_1:36
  f is special alternating & 1<=i & i+2<=len f implies f/.(i+1)
  is_extremal_in LSeg(f,i) \/ LSeg(f,i+1);

theorem :: SPPOL_1:37
  for u being Point of Euclid 2 st f is special alternating & 1<=i
  & i+2<=len f & u = f/.(i+1) & f/.(i+1) in LSeg(p,q) & f/.(i+1)<>q & not p in
  LSeg(f,i) \/ LSeg(f,i+1) holds for s st s>0 ex p3 st not p3 in LSeg(f,i) \/
  LSeg(f,i+1) & p3 in LSeg(p,q) & p3 in Ball(u,s);

definition
  let f1,f2,P;
  pred f1,f2 are_generators_of P means
:: SPPOL_1:def 5

  f1 is alternating being_S-Seq &
f2 is alternating being_S-Seq & f1/.1 = f2/.1 & f1/.len f1 = f2/.len f2 & <*f1
/.2,f1/.1,f2/.2*> is alternating & <*f1/.(len f1 - 1),f1/.len f1,f2/.(len f2 -
1)*> is alternating & f1/.1 <> f1/.len f1 & L~f1 /\ L~f2 = {f1/.1,f1/.len f1} &
  P = L~f1 \/ L~f2;
end;

theorem :: SPPOL_1:38
  f1,f2 are_generators_of P & 1<i & i<len f1 implies f1/.i is_extremal_in P;

:: Moved from KURATO_2, AK, 22.02.2006

theorem :: SPPOL_1:39
  for p, q being Point of TOP-REAL n, p9, q9 being Point of Euclid n st
  p = p9 & q = q9 holds dist (p9, q9) = |. p - q .|;

:: Moved from SPRECT_3, AK, 22.02.2006

theorem :: SPPOL_1:40
  for p,q,r being Point of TOP-REAL 2 st LSeg(p,q) is horizontal & r in
  LSeg(p,q) holds p`2 = r`2;

theorem :: SPPOL_1:41
  for p,q,r being Point of TOP-REAL 2 st LSeg(p,q) is vertical & r in
  LSeg(p,q) holds p`1 = r`1;

registration
  cluster compact non empty horizontal for Subset of TOP-REAL 2;
  cluster compact non empty vertical for Subset of TOP-REAL 2;
end;