:: The Topological Space ${\calE}^2_{\rm T}$. Simple Closed Curves
::  by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received December 30, 1991
:: Copyright (c) 1991-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, PRE_TOPC, EUCLID, FINSEQ_1, XBOOLE_0, RLTOPSP1, CARD_1,
      MCART_1, XXREAL_0, TOPREAL1, SUBSET_1, TARSKI, ARYTM_3, RCOMP_1,
      BORSUK_1, FUNCT_1, RELAT_1, TOPS_2, ORDINAL2, STRUCT_0, PARTFUN1,
      FUNCT_4, TOPREAL2, FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, FUNCT_4, ORDINAL1, NUMBERS, XXREAL_0, FINSEQ_1, STRUCT_0,
      PRE_TOPC, TOPS_2, COMPTS_1, RLTOPSP1, EUCLID, TOPMETR, TOPREAL1;
 constructors FUNCT_4, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, CONVEX1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, XXREAL_0, STRUCT_0,
      PRE_TOPC, BORSUK_1, EUCLID, TOPREAL1, RLTOPSP1, XREAL_0, ORDINAL1;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

reserve a for set;
reserve p,p1,p2,q,q1,q2 for Point of TOP-REAL 2;
reserve h1,h2 for FinSequence of TOP-REAL 2;

theorem :: TOPREAL2:1
  p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square implies
  ex P1, P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of p1,p2 & P2
  is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2};

theorem :: TOPREAL2:2
  R^2-unit_square is compact;

theorem :: TOPREAL2:3
  for Q, P being non empty Subset of TOP-REAL 2 for f being
  Function of (TOP-REAL 2)|Q, (TOP-REAL 2)|P st f is being_homeomorphism & Q
  is_an_arc_of q1,q2 holds for p1, p2 st p1 = f.q1 & p2 = f.q2 holds P
  is_an_arc_of p1,p2;

definition
  let P be Subset of TOP-REAL 2;
  attr P is being_simple_closed_curve means
:: TOPREAL2:def 1

  ex f being Function of (
  TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P st f is being_homeomorphism;
end;

registration
  cluster R^2-unit_square -> being_simple_closed_curve;
end;

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

definition
  mode Simple_closed_curve is being_simple_closed_curve Subset of TOP-REAL 2;
end;

theorem :: TOPREAL2:4
  for P being non empty Subset of TOP-REAL 2 st P is
  being_simple_closed_curve ex p1,p2 st p1 <> p2 & p1 in P & p2 in P;

theorem :: TOPREAL2:5
  for P being non empty Subset of TOP-REAL 2 holds P is
being_simple_closed_curve iff (ex p1,p2 st p1 <> p2 & p1 in P & p2 in P) & for
  p1,p2 st p1 <> p2 & p1 in P & p2 in P ex P1,P2 being non empty Subset of
TOP-REAL 2 st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1
  /\ P2 = {p1,p2};

theorem :: TOPREAL2:6
  for P being non empty Subset of TOP-REAL 2 holds P is
  being_simple_closed_curve iff ex p1,p2 being Point of TOP-REAL 2, P1,P2 being
  non empty Subset of TOP-REAL 2 st p1 <> p2 & p1 in P & p2 in P & P1
is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2};

registration
  cluster being_simple_closed_curve -> non empty compact for
Subset of TOP-REAL 2;
end;