:: On Rectangular Finite Sequences of the Points of the Plane
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received November 30, 1997
:: Copyright (c) 1997-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, XBOOLE_0, FUNCT_1, FINSEQ_1, CARD_1, ORDINAL4, RELAT_1,
      TARSKI, ZFMISC_1, PRE_TOPC, SUBSET_1, CONNSP_1, STRUCT_0, EUCLID,
      RCOMP_1, TOPREAL1, RLTOPSP1, PARTFUN1, ARYTM_3, SPPOL_1, SPPOL_2,
      MCART_1, PSCOMP_1, XXREAL_0, REAL_1, FINSEQ_6, GOBOARD5, ORDINAL2, NAT_1,
      GOBOARD1, GOBOARD2, MATRIX_1, TREES_1, COMPLEX1, ARYTM_1, XXREAL_1,
      XXREAL_2, JORDAN1, GOBOARD9, TOPS_1, SPRECT_1, SEQ_4;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1,
      NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1,
      RELSET_1, FINSEQ_1, FINSEQ_4, FINSEQ_6, XXREAL_0, XXREAL_2, SEQM_3,
      SEQ_4, MATRIX_0, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1,
      RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, JORDAN1, GOBOARD1, GOBOARD2,
      GOBOARD5, GOBOARD9, SPPOL_1, SPPOL_2, PSCOMP_1;
 constructors REAL_1, COMPLEX1, RCOMP_1, FINSEQ_4, REALSET1, TOPS_1, CONNSP_1,
      COMPTS_1, TOPREAL4, GOBOARD2, SPPOL_1, JORDAN1, SPPOL_2, PSCOMP_1,
      GOBOARD9, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, RVSUM_1, MEASURE6,
      SQUARE_1, COMSEQ_2;
 registrations XBOOLE_0, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, SEQ_2,
      FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, SPPOL_2,
      PSCOMP_1, WAYBEL_2, VALUED_0, XXREAL_2, COMPTS_1, FUNCT_1, RLTOPSP1,
      SEQ_4, SUBSET_1, RELSET_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

registration
  cluster non empty constant for FinSequence;
end;

theorem :: SPRECT_1:1
  for f,g being FinSequence st f^g is constant holds f is constant
  & g is constant;

theorem :: SPRECT_1:2
  for x,y being set st <*x,y*> is constant holds x = y;

theorem :: SPRECT_1:3
  for x,y,z being set st <*x,y,z*> is constant holds x = y & y = z & z = x;

begin :: Topology

theorem :: SPRECT_1:4
  for GX being non empty TopSpace, A being Subset of GX, B being
  non empty Subset of GX holds A is_a_component_of B implies A <> {};

theorem :: SPRECT_1:5
  for GX being TopStruct, A, B being Subset of GX holds A
  is_a_component_of B implies A c= B;

theorem :: SPRECT_1:6
  for T being non empty TopSpace, A being non empty Subset of T, B1
,B2,S being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & S
  is_a_component_of A & B1 \/ B2 = A holds S = B1 or S = B2;

theorem :: SPRECT_1:7
  for T being non empty TopSpace, A being non empty Subset of T, B1
,B2,C1,C2 being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A
& C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A
  holds { B1,B2 } = { C1,C2 };

begin :: Topology of Plane

reserve S for Subset of TOP-REAL 2,
  C,C1,C2 for non empty compact Subset of TOP-REAL 2,
  p,q for Point of TOP-REAL 2;

theorem :: SPRECT_1:8
  for p,q,r being Point of TOP-REAL 2 holds L~<*p,q,r*> = LSeg(p,q
  ) \/ LSeg(q,r);

registration
  let n be Nat;
  let f be non trivial FinSequence of TOP-REAL n;
  cluster L~f -> non empty;
end;

registration
  let f be FinSequence of TOP-REAL 2;
  cluster L~f -> compact;
end;

theorem :: SPRECT_1:9
  for A,B being Subset of TOP-REAL 2 st A c= B & B is horizontal
  holds A is horizontal;

theorem :: SPRECT_1:10
  for A,B being Subset of TOP-REAL 2 st A c= B & B is vertical
  holds A is vertical;

registration
  cluster R^2-unit_square -> special_polygonal non horizontal non vertical;
end;

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

begin :: Special points of a compact non empty subset of the plane

theorem :: SPRECT_1:11
  N-min C in C & N-max C in C;

theorem :: SPRECT_1:12
  S-min C in C & S-max C in C;

theorem :: SPRECT_1:13
  W-min C in C & W-max C in C;

theorem :: SPRECT_1:14
  E-min C in C & E-max C in C;

theorem :: SPRECT_1:15
  C is vertical iff W-bound C = E-bound C;

theorem :: SPRECT_1:16
  C is horizontal iff S-bound C = N-bound C;

theorem :: SPRECT_1:17
  NW-corner C = NE-corner C implies C is vertical;

theorem :: SPRECT_1:18
  SW-corner C = SE-corner C implies C is vertical;

theorem :: SPRECT_1:19
  NW-corner C = SW-corner C implies C is horizontal;

theorem :: SPRECT_1:20
  NE-corner C = SE-corner C implies C is horizontal;

reserve i,j,k for Nat,
  t,r1,r2,s1,s2 for Real;

theorem :: SPRECT_1:21
  W-bound C <= E-bound C;

theorem :: SPRECT_1:22
  S-bound C <= N-bound C;

theorem :: SPRECT_1:23
  LSeg(SE-corner C, NE-corner C) = { p : p`1 = E-bound C & p`2 <=
  N-bound C & p`2 >= S-bound C };

theorem :: SPRECT_1:24
  LSeg(SW-corner C, SE-corner C) = { p : p`1 <= E-bound C & p`1 >=
  W-bound C & p`2 = S-bound C};

theorem :: SPRECT_1:25
  LSeg(NW-corner C, NE-corner C) = { p : p`1 <= E-bound C & p`1 >=
  W-bound C & p`2 = N-bound C};

theorem :: SPRECT_1:26
  LSeg(SW-corner C, NW-corner C) = { p : p`1 = W-bound C & p`2 <=
  N-bound C & p`2 >= S-bound C};

theorem :: SPRECT_1:27
  LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C) = {
  NW-corner C };

theorem :: SPRECT_1:28
  LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C) =
  {NE-corner C};

theorem :: SPRECT_1:29
  LSeg(SE-corner C,NE-corner C) /\ LSeg(SW-corner C,SE-corner C) =
  {SE-corner C};

theorem :: SPRECT_1:30
  LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C) =
  {SW-corner C};

begin :: Neither vertical nor horizontal

reserve D1 for non vertical non empty compact Subset of TOP-REAL 2,
  D2 for non horizontal non empty compact Subset of TOP-REAL 2,
  D for non vertical non horizontal non empty compact Subset of TOP-REAL 2;

theorem :: SPRECT_1:31
  W-bound D1 < E-bound D1;

theorem :: SPRECT_1:32
  S-bound D2 < N-bound D2;

theorem :: SPRECT_1:33
  LSeg(SW-corner D1,NW-corner D1) misses LSeg(SE-corner D1, NE-corner D1);

theorem :: SPRECT_1:34
  LSeg(SW-corner D2,SE-corner D2) misses LSeg(NW-corner D2, NE-corner D2);

begin :: SpStSeq

definition
  let C be Subset of TOP-REAL 2;
  func SpStSeq C -> FinSequence of TOP-REAL 2 equals
:: SPRECT_1:def 1
  <*NW-corner C,NE-corner C
  ,SE-corner C*>^ <*SW-corner C,NW-corner C*>;
end;

theorem :: SPRECT_1:35
  (SpStSeq S)/.1 = NW-corner S;

theorem :: SPRECT_1:36
  (SpStSeq S)/.2 = NE-corner S;

theorem :: SPRECT_1:37
  (SpStSeq S)/.3 = SE-corner S;

theorem :: SPRECT_1:38
  (SpStSeq S)/.4 = SW-corner S;

theorem :: SPRECT_1:39
  (SpStSeq S)/.5 = NW-corner S;

theorem :: SPRECT_1:40
  len SpStSeq S = 5;

theorem :: SPRECT_1:41
  L~SpStSeq S = (LSeg(NW-corner S,NE-corner S) \/ LSeg(NE-corner S
,SE-corner S)) \/ (LSeg(SE-corner S,SW-corner S) \/ LSeg(SW-corner S,NW-corner
  S));

registration
  let D be non vertical non empty compact Subset of TOP-REAL 2;
  cluster SpStSeq D -> non constant;
end;

registration
  let D be non horizontal non empty compact Subset of TOP-REAL 2;
  cluster SpStSeq D -> non constant;
end;

registration
  let D be non vertical non horizontal non empty compact Subset of TOP-REAL 2;
  cluster SpStSeq D -> special unfolded circular s.c.c. standard;
end;

theorem :: SPRECT_1:42
  L~SpStSeq D = [.W-bound D,E-bound D,S-bound D,N-bound D.];

registration
  let T be non empty TopSpace, X be non empty compact Subset of T,
      f be continuous RealMap of T;
  cluster f.:X -> bounded_below;
 cluster f.:X -> bounded_above;
end;

theorem :: SPRECT_1:43
  W-bound S = lower_bound(proj1.:S);

theorem :: SPRECT_1:44
  S-bound S = lower_bound(proj2.:S);

theorem :: SPRECT_1:45
  N-bound S = upper_bound(proj2.:S);

theorem :: SPRECT_1:46
  E-bound S = upper_bound(proj1.:S);

theorem :: SPRECT_1:47
  S = C1 \/ C2 implies W-bound S = min(W-bound C1, W-bound C2);

theorem :: SPRECT_1:48
  S = C1 \/ C2 implies S-bound S = min(S-bound C1, S-bound C2);

theorem :: SPRECT_1:49
  S = C1 \/ C2 implies N-bound S = max(N-bound C1, N-bound C2);

theorem :: SPRECT_1:50
  S = C1 \/ C2 implies E-bound S = max(E-bound C1, E-bound C2);

registration
  let r1,r2 be Real;
  cluster [.r1,r2.] -> real-bounded for Subset of REAL;
end;

theorem :: SPRECT_1:51
  r1 <= r2 implies (t in [.r1,r2.] iff ex s1 st 0 <=s1 & s1 <= 1 &
  t = s1*r1 + (1-s1)*r2);

theorem :: SPRECT_1:52
  p`1 <= q`1 implies proj1.:LSeg(p,q) = [.p`1,q`1.];

theorem :: SPRECT_1:53
  p`2 <= q`2 implies proj2.:LSeg(p,q) = [.p`2,q`2.];

theorem :: SPRECT_1:54
  p`1 <= q`1 implies W-bound LSeg(p,q) = p`1;

theorem :: SPRECT_1:55
  p`2 <= q`2 implies S-bound LSeg(p,q) = p`2;

theorem :: SPRECT_1:56
  p`2 <= q`2 implies N-bound LSeg(p,q) = q`2;

theorem :: SPRECT_1:57
  p`1 <= q`1 implies E-bound LSeg(p,q) = q`1;

theorem :: SPRECT_1:58
  W-bound L~SpStSeq C = W-bound C;

theorem :: SPRECT_1:59
  S-bound L~SpStSeq C = S-bound C;

theorem :: SPRECT_1:60
  N-bound L~SpStSeq C = N-bound C;

theorem :: SPRECT_1:61
  E-bound L~SpStSeq C = E-bound C;

theorem :: SPRECT_1:62
  NW-corner L~SpStSeq C = NW-corner C;

theorem :: SPRECT_1:63
  NE-corner L~SpStSeq C = NE-corner C;

theorem :: SPRECT_1:64
  SW-corner L~SpStSeq C = SW-corner C;

theorem :: SPRECT_1:65
  SE-corner L~SpStSeq C = SE-corner C;

theorem :: SPRECT_1:66
  W-most L~SpStSeq C = LSeg(SW-corner C,NW-corner C);

theorem :: SPRECT_1:67
  N-most L~SpStSeq C = LSeg(NW-corner C,NE-corner C);

theorem :: SPRECT_1:68
  S-most L~SpStSeq C = LSeg(SW-corner C,SE-corner C);

theorem :: SPRECT_1:69
  E-most L~SpStSeq C = LSeg(SE-corner C,NE-corner C);

theorem :: SPRECT_1:70
  proj2.:LSeg(SW-corner C,NW-corner C) = [.S-bound C,N-bound C.];

theorem :: SPRECT_1:71
  proj1.:LSeg(NW-corner C,NE-corner C) = [.W-bound C,E-bound C.];

theorem :: SPRECT_1:72
  proj2.:LSeg(NE-corner C,SE-corner C) = [.S-bound C,N-bound C.];

theorem :: SPRECT_1:73
  proj1.:LSeg(SE-corner C,SW-corner C) = [.W-bound C,E-bound C.];

theorem :: SPRECT_1:74
  W-min L~SpStSeq C = SW-corner C;

theorem :: SPRECT_1:75
  W-max L~SpStSeq C = NW-corner C;

theorem :: SPRECT_1:76
  N-min L~SpStSeq C = NW-corner C;

theorem :: SPRECT_1:77
  N-max L~SpStSeq C = NE-corner C;

theorem :: SPRECT_1:78
  E-min L~SpStSeq C = SE-corner C;

theorem :: SPRECT_1:79
  E-max L~SpStSeq C = NE-corner C;

theorem :: SPRECT_1:80
  S-min L~SpStSeq C = SW-corner C;

theorem :: SPRECT_1:81
  S-max L~SpStSeq C = SE-corner C;

begin :: rectangular

definition
  let f be FinSequence of TOP-REAL 2;
  attr f is rectangular means
:: SPRECT_1:def 2

  ex D st f = SpStSeq D;
end;

registration
  let D;
  cluster SpStSeq D -> rectangular;
end;

registration
  cluster rectangular for FinSequence of TOP-REAL 2;
end;

reserve s for rectangular FinSequence of TOP-REAL 2;

theorem :: SPRECT_1:82
  len s = 5;

registration
  cluster rectangular -> non constant for FinSequence of TOP-REAL 2;
end;

registration
  cluster rectangular -> standard special unfolded circular s.c.c. for
non empty
    FinSequence of TOP-REAL 2;
end;

:: Special points of L~f, f - rectangular

theorem :: SPRECT_1:83
  s/.1 = N-min L~s & s/.1 = W-max L~s;

theorem :: SPRECT_1:84
  s/.2 = N-max L~s & s/.2 = E-max L~s;

theorem :: SPRECT_1:85
  s/.3 = S-max L~s & s/.3 = E-min L~s;

theorem :: SPRECT_1:86
  s/.4 = S-min L~s & s/.4 = W-min L~s;

begin :: Jordan

theorem :: SPRECT_1:87
  r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan;

registration
  let f be rectangular FinSequence of TOP-REAL 2;
  cluster L~f -> Jordan;
end;

definition
  let S be Subset of TOP-REAL 2;
  redefine attr S is Jordan means
:: SPRECT_1:def 3

  S`<> {} & ex A1,A2 being Subset of
  TOP-REAL 2 st S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1
  is_a_component_of S` & A2 is_a_component_of S`;
end;

theorem :: SPRECT_1:88
  for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp
  f misses RightComp f;

registration
  let f be non constant standard special_circular_sequence;
  cluster LeftComp f -> non empty;
  cluster RightComp f -> non empty;
end;

theorem :: SPRECT_1:89
  for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp f <>
  RightComp f;