:: Left and Right Component of the Complement of a Special Closed Curve
::  by Andrzej Trybulec
::
:: Received October 29, 1995
:: Copyright (c) 1995-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, FUNCT_1, GOBOARD5, SUBSET_1, REAL_1, PRE_TOPC, EUCLID,
      GOBOARD1, CONNSP_1, XBOOLE_0, RELAT_1, STRUCT_0, TARSKI, RELAT_2,
      RLTOPSP1, CONVEX1, FINSEQ_1, FINSEQ_5, ARYTM_3, ARYTM_1, XXREAL_0,
      PARTFUN1, MCART_1, GOBOARD2, CARD_1, MATRIX_1, COMPLEX1, TREES_1, TOPS_1,
      TOPREAL1, GOBOARD9, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
      COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1,
      MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, RLVECT_1,
      RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, FINSEQ_5, GOBOARD5,
      XXREAL_0;
 constructors REAL_1, FINSEQ_5, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD5, GOBOARD1,
      NAT_D, RELSET_1, CONVEX1, RVSUM_1, SEQ_4;
 registrations RELSET_1, NUMBERS, XXREAL_0, FINSEQ_1, FINSEQ_6, STRUCT_0,
      PRE_TOPC, EUCLID, GOBOARD2, GOBOARD5, ORDINAL1, RLTOPSP1, JORDAN1,
      XREAL_0, INT_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve f for non constant standard special_circular_sequence,
  i,j,k,i1,i2,j1,j2 for Nat,
  r,s,r1,s1,r2,s2 for Real,
  p,q for Point of TOP-REAL 2,
  G for Go-board;

theorem :: GOBOARD9:1
  for GX being TopSpace, A1,A2,B being Subset of GX
  st A1 is_a_component_of B & A2 is_a_component_of B holds
  A1 = A2 or A1 misses A2;

theorem :: GOBOARD9:2
  for GX being TopSpace, A,B being Subset of GX,
  AA being Subset of GX|B st A = AA holds GX|A = GX|B|AA;

theorem :: GOBOARD9:3
  for GX being non empty TopSpace, A, B being non empty Subset of GX
  st A c= B & A is connected
  ex C being Subset of GX st C is_a_component_of B & A c= C;

theorem :: GOBOARD9:4
  for GX being non empty TopSpace, A,B,C,D being Subset of GX
  st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D
  holds B c= C;

registration
  cluster convex non empty for Subset of TOP-REAL 2;
end;

::$CT

theorem :: GOBOARD9:6  :: ouogolnic !!!
  for P,Q being convex Subset of TOP-REAL 2 holds P /\ Q is convex;

theorem :: GOBOARD9:7
  for f being FinSequence of TOP-REAL 2 holds Rev X_axis f = X_axis Rev f;

theorem :: GOBOARD9:8
  for f being FinSequence of TOP-REAL 2 holds Rev Y_axis f = Y_axis Rev f;

registration
  cluster non constant for FinSequence;
end;

registration
  let f be non constant FinSequence;
  cluster Rev f -> non constant;
end;

definition
  let f be standard special_circular_sequence;
  redefine func Rev f -> standard special_circular_sequence;
end;

theorem :: GOBOARD9:9
  i >= 1 & j >= 1 & i+j = len f implies left_cell(f,i) = right_cell(Rev f,j);

theorem :: GOBOARD9:10
  i >= 1 & j >= 1 & i+j = len f implies left_cell(Rev f,i) = right_cell(f,j);

theorem :: GOBOARD9:11
  1 <= k & k+1 <= len f implies ex i,j st i <= len GoB f & j <= width GoB f &
  cell(GoB f,i,j) = left_cell(f,k);

theorem :: GOBOARD9:12
  j <= width G implies Int h_strip(G,j) is convex;

theorem :: GOBOARD9:13
  i <= len G implies Int v_strip(G,i) is convex;

theorem :: GOBOARD9:14
  i <= len G & j <= width G implies Int cell(G,i,j) <> {};

theorem :: GOBOARD9:15
  1 <= k & k+1 <= len f implies Int left_cell(f,k) <> {};

theorem :: GOBOARD9:16
  1 <= k & k+1 <= len f implies Int right_cell(f,k) <> {};

theorem :: GOBOARD9:17
  i <= len G & j <= width G implies Int cell(G,i,j) is convex;

::$CT

theorem :: GOBOARD9:19
  1 <= k & k+1 <= len f implies Int left_cell(f,k) is convex;

theorem :: GOBOARD9:20
  1 <= k & k+1 <= len f implies Int right_cell(f,k) is convex;

definition
  let f;
  func LeftComp f -> Subset of TOP-REAL 2 means
:: GOBOARD9:def 1

  it is_a_component_of (L~f)` & Int left_cell(f,1) c= it;
  func RightComp f -> Subset of TOP-REAL 2 means
:: GOBOARD9:def 2

  it is_a_component_of (L~f)` & Int right_cell(f,1) c= it;
end;

theorem :: GOBOARD9:21
  for k st 1 <= k & k+1 <= len f holds Int left_cell(f,k) c= LeftComp f;

theorem :: GOBOARD9:22
  GoB Rev f = GoB f;

theorem :: GOBOARD9:23
  RightComp f = LeftComp Rev f;

theorem :: GOBOARD9:24
  RightComp Rev f = LeftComp f;

theorem :: GOBOARD9:25
  for k st 1 <= k & k+1 <= len f holds Int right_cell(f,k) c= RightComp f;