:: On Some Points of a Simple Closed Curve. {P}art {II}
::  by Artur Korni{\l}owicz and Adam Grabowski
::
:: Received October 6, 2004
:: Copyright (c) 2004-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, TOPREAL2, SUBSET_1, EUCLID, RELAT_1, PRE_TOPC, FUNCT_1,
      STRUCT_0, JORDAN19, TARSKI, GOBOARD9, JORDAN9, CARD_1, JORDAN6, TOPREAL1,
      RELAT_2, PSCOMP_1, RCOMP_1, KURATO_2, XBOOLE_0, XXREAL_0, FINSEQ_1,
      JORDAN8, MATRIX_1, TREES_1, SPPOL_1, ARYTM_3, METRIC_1, ARYTM_1, NEWTON,
      ORDINAL2, RLTOPSP1, JORDAN1A, MCART_1, XXREAL_2, SEQ_4, GOBOARD2,
      JORDAN21, JORDAN2C, GOBOARD1, FINSEQ_6, GOBOARD5, PARTFUN1, PCOMPS_1,
      WEIERSTR, SEQ_1, SEQ_2, REAL_1, COMPLEX1, JORDAN10, JORDAN3, CONVEX1,
      NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0,
      XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, RELSET_1, PARTFUN1,
      FUNCT_2, XXREAL_2, SEQ_4, NEWTON, FINSEQ_1, MATRIX_0, DOMAIN_1, STRUCT_0,
      PRE_TOPC, COMPTS_1, FINSEQ_6, CONNSP_1, METRIC_1, PCOMPS_1, PSCOMP_1,
      RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD2,
      WEIERSTR, SPPOL_1, GOBOARD5, TOPRNS_1, JORDAN2C, JORDAN6, GOBOARD9,
      JORDAN8, JORDAN9, GOBRD13, TOPREAL6, JORDAN10, JORDAN1K, JORDAN1A,
      KURATO_2, JORDAN19, JORDAN21;
 constructors REAL_1, RCOMP_1, NEWTON, BINARITH, CONNSP_1, MONOID_0, TOPRNS_1,
      TOPREAL4, GOBOARD2, PSCOMP_1, GOBOARD9, JORDAN5C, JORDAN6, JORDAN2C,
      TOPREAL6, JORDAN1K, JORDAN21, JORDAN8, GOBRD13, JORDAN9, JORDAN10,
      JORDAN1A, KURATO_2, JORDAN19, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, JORDAN11;
 registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2,
      GOBOARD2, SPPOL_2, TOPREAL5, SPRECT_2, JORDAN6, SPRECT_3, JORDAN2C,
      REVROT_1, TOPREAL6, JORDAN21, JORDAN8, JORDAN10, VALUED_0, FUNCT_1,
      ORDINAL1, RLTOPSP1, JORDAN1, XCMPLX_0, NEWTON;
 requirements SUBSET, BOOLE, REAL, NUMERALS, ARITHM;


begin :: Properties of the Approximations

reserve C for Simple_closed_curve,
  i for Nat;

theorem :: JORDAN22:1
  (Upper_Appr C).i c= Cl RightComp Cage(C,0);

theorem :: JORDAN22:2
  (Lower_Appr C).i c= Cl RightComp Cage(C,0);

registration
  let C be Simple_closed_curve;
  cluster Upper_Arc C -> connected;
  cluster Lower_Arc C -> connected;
end;

theorem :: JORDAN22:3
  (Upper_Appr C).i is compact connected;

theorem :: JORDAN22:4
  (Lower_Appr C).i is compact connected;

registration
  let C be Simple_closed_curve;
  cluster North_Arc C -> compact;
  cluster South_Arc C -> compact;
end;

:: Moved from JORDAN21, AK, 22.02.2006

reserve R for non empty Subset of TOP-REAL 2,
  j, k, m, n for Nat;

theorem :: JORDAN22:5
  [1,1] in Indices Gauge(R,n);

theorem :: JORDAN22:6
  [1,2] in Indices Gauge(R,n);

theorem :: JORDAN22:7
  [2,1] in Indices Gauge(R,n);

theorem :: JORDAN22:8
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k & [i,j] in Indices Gauge(C,k) & [i,j+1] in Indices Gauge
(C,k) implies dist(Gauge(C,m)*(i,j),Gauge(C,m)*(i,j+1)) < dist(Gauge(C,k)*(i,j)
  ,Gauge(C,k)*(i,j+1));

theorem :: JORDAN22:9
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k implies dist(Gauge(C,m)*(1,1),Gauge(C,m)*(1,2)) < dist(
  Gauge(C,k)*(1,1),Gauge(C,k)*(1,2));

theorem :: JORDAN22:10
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k & [i,j] in Indices Gauge(C,k) & [i+1,j] in Indices Gauge
(C,k) implies dist(Gauge(C,m)*(i,j),Gauge(C,m)*(i+1,j)) < dist(Gauge(C,k)*(i,j)
  ,Gauge(C,k)*(i+1,j));

theorem :: JORDAN22:11
  for C being non vertical non horizontal compact Subset of
TOP-REAL 2 holds m > k implies dist(Gauge(C,m)*(1,1),Gauge(C,m)*(2,1)) < dist(
  Gauge(C,k)*(1,1),Gauge(C,k)*(2,1));

theorem :: JORDAN22:12
  for r, t being Real holds r > 0 & t > 0 implies ex n being
  Nat st i < n & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r & dist(
  Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < t;

theorem :: JORDAN22:13
  0 < n implies upper_bound (proj2.:(L~Cage(C,n) /\ LSeg(Gauge(C,n)*(
Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))))
 = upper_bound (
proj2.:(L~Cage(C,n) /\ Vertical_Line ((E-bound L~Cage(C,n) + W-bound L~Cage(C,n
  )) / 2)));

theorem :: JORDAN22:14
  0 < n implies lower_bound (proj2.:(L~Cage(C,n) /\ LSeg(Gauge(C,n)*(
Center Gauge(C,n),1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))))
 = lower_bound (
proj2.:(L~Cage(C,n) /\ Vertical_Line ((E-bound L~Cage(C,n) + W-bound L~Cage(C,n
  )) / 2)));

theorem :: JORDAN22:15
  0 < n implies UMP L~Cage(C,n) = |[ (E-bound L~Cage(C,n) + W-bound L~
Cage(C,n)) / 2, upper_bound (proj2.:(L~Cage(C,n) /\
 LSeg(Gauge(C,n)*(Center Gauge(C,n),
  1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))))) ]|;

theorem :: JORDAN22:16
  0 < n implies LMP L~Cage(C,n) = |[ (E-bound L~Cage(C,n) + W-bound L~
Cage(C,n)) / 2, lower_bound (proj2.:(L~Cage(C,n) /\
 LSeg(Gauge(C,n)*(Center Gauge(C,n),
  1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))))) ]|;

theorem :: JORDAN22:17
  (UMP C)`2 < (UMP L~Cage(C,n))`2;

theorem :: JORDAN22:18
  (LMP C)`2 > (LMP L~Cage(C,n))`2;

theorem :: JORDAN22:19
  0 < n implies ex i being Nat st 1 <= i & i <= len
  Gauge(C,n) & UMP L~Cage(C,n) = Gauge(C,n)*(Center Gauge(C,n),i);

theorem :: JORDAN22:20
  0 < n implies ex i being Nat st 1 <= i & i <= len
  Gauge(C,n) & LMP L~Cage(C,n) = Gauge(C,n)*(Center Gauge(C,n),i);

theorem :: JORDAN22:21
  0 < n implies UMP L~Cage(C,n) = UMP Upper_Arc L~Cage(C,n);

theorem :: JORDAN22:22
  0 < n implies LMP L~Cage(C,n) = LMP Lower_Arc L~Cage(C,n);

theorem :: JORDAN22:23
  0 < n implies (UMP C)`2 < (UMP Upper_Arc L~Cage(C,n))`2;

theorem :: JORDAN22:24
  0 < n implies (LMP Lower_Arc L~Cage(C,n))`2 < (LMP C)`2;

theorem :: JORDAN22:25
  i <= j implies (UMP L~Cage(C,j))`2 <= (UMP L~Cage(C,i))`2;

theorem :: JORDAN22:26
  i <= j implies (LMP L~Cage(C,i))`2 <= (LMP L~Cage(C,j))`2;

theorem :: JORDAN22:27
  0 < i & i <= j implies (UMP Upper_Arc L~Cage(C,j))`2 <= (UMP
  Upper_Arc L~Cage(C,i))`2;

theorem :: JORDAN22:28
  0 < i & i <= j implies (LMP Lower_Arc L~Cage(C,i))`2 <= (LMP
  Lower_Arc L~Cage(C,j))`2;

begin :: On Special Points of Approximations

theorem :: JORDAN22:29
  W-min C in North_Arc C;

theorem :: JORDAN22:30
  E-max C in North_Arc C;

theorem :: JORDAN22:31
  W-min C in South_Arc C;

theorem :: JORDAN22:32
  E-max C in South_Arc C;

theorem :: JORDAN22:33
  UMP C in North_Arc C;

theorem :: JORDAN22:34
  LMP C in South_Arc C;

theorem :: JORDAN22:35
  North_Arc C c= C;

theorem :: JORDAN22:36
  South_Arc C c= C;

theorem :: JORDAN22:37
  LMP C in Lower_Arc C & UMP C in Upper_Arc C or UMP C in Lower_Arc C &
  LMP C in Upper_Arc C;

:: Moved from JORDAN, AG 20.01.2006

theorem :: JORDAN22:38
  W-bound C = W-bound North_Arc C;

theorem :: JORDAN22:39
  E-bound C = E-bound North_Arc C;

theorem :: JORDAN22:40
  W-bound C = W-bound South_Arc C;

theorem :: JORDAN22:41
  E-bound C = E-bound South_Arc C;