:: On the Decompositions of Intervals and Simple Closed Curves
::  by Adam Grabowski
::
:: Received August 7, 2002
:: Copyright (c) 2002-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, ZFMISC_1, TOPREAL2, PRE_TOPC, EUCLID, XBOOLE_0,
      SUBSET_1, TARSKI, STRUCT_0, FUNCT_1, RELAT_1, FUNCT_4, PARTFUN1,
      TOPREAL1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, BORSUK_1, XXREAL_1,
      TOPMETR, CONNSP_1, REAL_1, RELAT_2, RCOMP_1, XXREAL_2, ORDINAL2, SEQ_4,
      T_0TOPSP, TOPS_2, RLTOPSP1, TREAL_1, VALUED_1, BORSUK_4, FUNCT_2,
      MEASURE5;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_2, XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      DOMAIN_1, RCOMP_1, FUNCT_4, XXREAL_0, STRUCT_0, MEASURE6, PRE_TOPC,
      COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, SEQ_4, TREAL_1, CONNSP_1,
      BORSUK_1, BORSUK_3, TSEP_1, TOPMETR, MEASURE5, TOPS_2;
 constructors FUNCT_4, CONNSP_1, TOPS_2, COMPTS_1, TSEP_1, TOPREAL1, TOPREAL2,
      TREAL_1, MEASURE6, BORSUK_3, INTEGRA1, SEQ_4, BINOP_2;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED,
      RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, EUCLID,
      TOPREAL1, TOPREAL2, BORSUK_2, REVROT_1, TOPREAL6, XXREAL_2, TOPMETR,
      SUBSET_1, MEASURE5, JORDAN2C, ORDINAL1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

registration
  cluster -> non trivial for Simple_closed_curve;
end;

::$CT 3

theorem :: BORSUK_4:4
  for f, g being Function, a being set st f is one-to-one & g is
one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } holds f +* g is
  one-to-one;

theorem :: BORSUK_4:5
  for f, g being Function, a being set st f is one-to-one & g is
  one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } & f.a = g.a
  holds (f +* g)" = f" +* g";

theorem :: BORSUK_4:6
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
  being Point of TOP-REAL n st A is_an_arc_of p, q holds A \ {p} is non empty;

theorem :: BORSUK_4:7
  for s1, s3, s4, l being Real st s1 <= s3 & s1 < s4 & 0 <= l & l
  <= 1 holds s1 <= (1-l) * s3+l*s4;

theorem :: BORSUK_4:8
  for A being Subset of I[01], a, b being Real st a < b & A
  = ].a,b.[ holds [.a,b.] c= the carrier of I[01];

theorem :: BORSUK_4:9
  for A being Subset of I[01], a, b being Real st a < b & A
  = ].a,b.] holds [.a,b.] c= the carrier of I[01];

theorem :: BORSUK_4:10
  for A being Subset of I[01], a, b being Real st a < b & A
  = [.a,b.[ holds [.a,b.] c= the carrier of I[01];

theorem :: BORSUK_4:11
  for a, b being Real st a <> b holds Cl ].a,b.] = [.a,b.];

theorem :: BORSUK_4:12
  for a, b being Real st a <> b holds Cl [.a,b.[ = [.a,b.];

theorem :: BORSUK_4:13
  for A being Subset of I[01], a, b being Real st a < b & A = ].a
  ,b.[ holds Cl A = [.a,b.];

theorem :: BORSUK_4:14
  for A being Subset of I[01], a, b being Real st a < b & A
  = ].a,b.] holds Cl A = [.a,b.];

theorem :: BORSUK_4:15
  for A being Subset of I[01], a, b being Real st a < b & A
  = [.a,b.[ holds Cl A = [.a,b.];

theorem :: BORSUK_4:16
  for A being Subset of I[01], a, b being Real st a <= b &
  A = [.a,b.] holds 0 <= a & b <= 1;

theorem :: BORSUK_4:17
  for A, B being Subset of I[01], a, b, c being Real st a <
  b & b < c & A = [.a,b.[ & B = ].b,c.] holds A, B are_separated;

theorem :: BORSUK_4:18
  for p1, p2 being Point of I[01] holds [. p1, p2 .] is Subset of I[01];

theorem :: BORSUK_4:19
  for a, b being Point of I[01] holds ]. a, b .[ is Subset of I[01];

begin :: Decompositions of Intervals

theorem :: BORSUK_4:20
  for p being Real holds {p} is non empty closed_interval Subset of REAL;

theorem :: BORSUK_4:21
  for A being non empty connected Subset of I[01], a, b, c being
  Point of I[01] st a <= b & b <= c & a in A & c in A holds b in A;

theorem :: BORSUK_4:22
  for A being non empty connected Subset of I[01], a, b being Real
 st a in A & b in A holds [.a,b.] c= A;

theorem :: BORSUK_4:23
  for a, b being Real, A being Subset of I[01] st A = [.a,b
  .] holds A is closed;

theorem :: BORSUK_4:24
  for p1, p2 being Point of I[01] st p1 <= p2 holds [. p1, p2 .]
  is non empty compact connected Subset of I[01];

theorem :: BORSUK_4:25
  for X being Subset of I[01], X9 being Subset of REAL st X9 = X
  holds X9 is bounded_above bounded_below;

theorem :: BORSUK_4:26
  for X being Subset of I[01], X9 being Subset of REAL, x being
  Real st x in X9 & X9 = X holds lower_bound X9 <= x &
   x <= upper_bound X9;

theorem :: BORSUK_4:27
  for A being Subset of REAL, B being Subset of I[01] st A = B
  holds A is closed iff B is closed;

theorem :: BORSUK_4:28
  for C being non empty closed_interval Subset of REAL
   holds lower_bound C <= upper_bound C;

theorem :: BORSUK_4:29
  for C being non empty compact connected Subset of I[01], C9
  being Subset of REAL st C = C9 &
   [. lower_bound C9, upper_bound C9 .] c= C9 holds [. lower_bound C9,
  upper_bound C9 .] = C9;

theorem :: BORSUK_4:30
  for C being non empty compact connected Subset of I[01] holds C
  is non empty closed_interval Subset of REAL;

theorem :: BORSUK_4:31
  for C being non empty compact connected Subset of I[01] ex p1,
  p2 being Point of I[01] st p1 <= p2 & C = [. p1, p2 .];

begin :: Decompositions of Simple Closed Curves

definition
  func I(01) -> strict SubSpace of I[01] means
:: BORSUK_4:def 1

  the carrier of it = ]. 0,1 .[;
end;

registration
  cluster I(01) -> non empty;
end;

theorem :: BORSUK_4:32
  for A being Subset of I[01] st A = the carrier of I(01) holds
  I(01) = I[01] | A;

theorem :: BORSUK_4:33
  the carrier of I(01) = (the carrier of I[01]) \ {0,1};

registration
  cluster I(01) -> open;
end;

theorem :: BORSUK_4:34
  I(01) is open;

theorem :: BORSUK_4:35
  for r being Real holds r in the carrier of I(01) iff 0 < r & r < 1;

theorem :: BORSUK_4:36
  for a, b being Point of I[01] st a < b & b <> 1 holds ]. a, b .]
  is non empty Subset of I(01);

theorem :: BORSUK_4:37
  for a, b being Point of I[01] st a < b & a <> 0 holds [. a, b .[
  is non empty Subset of I(01);

theorem :: BORSUK_4:38
  for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,
  (TOP-REAL 2) | D are_homeomorphic;

theorem :: BORSUK_4:39
  for n being Element of NAT, D being non empty Subset of TOP-REAL n, p1
, p2 being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I(01), (TOP-REAL
  n) | (D \ {p1,p2}) are_homeomorphic;

theorem :: BORSUK_4:40
  for n being Element of NAT, D being Subset of TOP-REAL n, p1, p2
being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I[01], (TOP-REAL n) |
  D are_homeomorphic;

theorem :: BORSUK_4:41
  for n being Element of NAT, p1, p2 being Point of TOP-REAL n st p1 <>
p2 holds I[01], (TOP-REAL n) | LSeg (p1, p2) are_homeomorphic;

theorem :: BORSUK_4:42
  for E being Subset of I(01) st (ex p1, p2 being Point of I[01]
  st p1 < p2 & E = [. p1,p2 .]) holds I[01], I(01)|E are_homeomorphic;

theorem :: BORSUK_4:43
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
  < b ex E being non empty Subset of I[01], f being Function of I[01]|E, (
TOP-REAL n)|A st E = [. a, b .] & f is being_homeomorphism & f.a = p & f.b = q;

theorem :: BORSUK_4:44
  for A being TopSpace, B being non empty TopSpace, f being
Function of A, B, C being TopSpace, X being Subset of A st f is continuous & C
  is SubSpace of B holds for h being Function of A|X, C st h = f|X holds h is
  continuous;

theorem :: BORSUK_4:45
  for X being Subset of I[01], a, b being Point of I[01] st X = ].
  a, b .[ holds X is open;

theorem :: BORSUK_4:46
  for X being Subset of I(01), a, b being Point of I[01] st X = ].
  a, b .[ holds X is open;

theorem :: BORSUK_4:47
  for X being Subset of I(01), a being Point of I[01] st X = ]. 0,
  a .] holds X is closed;

theorem :: BORSUK_4:48
  for X being Subset of I(01), a being Point of I[01] st X = [. a,
  1 .[ holds X is closed;

theorem :: BORSUK_4:49
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & b <> 1 ex E being non empty Subset of I(01), f being Function of I(01)|E,
  (TOP-REAL n)|(A \ {p}) st E = ]. a, b .] & f is being_homeomorphism & f.b = q
;

theorem :: BORSUK_4:50
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & a <> 0 ex E being non empty Subset of I(01), f being Function of I(01)|E,
  (TOP-REAL n)|(A \ {q}) st E = [. a, b .[ & f is being_homeomorphism & f.a = p
;

theorem :: BORSUK_4:51
  for n being Element of NAT, A, B being Subset of TOP-REAL n, p,
q being Point of TOP-REAL n st A is_an_arc_of p, q & B is_an_arc_of q, p & A /\
  B = { p, q } & p <> q holds I(01), (TOP-REAL n) | ((A \ {p}) \/ (B \ {p}))
  are_homeomorphic;

theorem :: BORSUK_4:52
  for D being Simple_closed_curve, p being Point of TOP-REAL 2 st
  p in D holds (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic;

theorem :: BORSUK_4:53
  for D being Simple_closed_curve, p, q being Point of TOP-REAL 2 st p
  in D & q in D holds (TOP-REAL 2) | (D \ {p}), (TOP-REAL 2) | (D \ {q})
  are_homeomorphic;

theorem :: BORSUK_4:54
  for n being Element of NAT, C being non empty Subset of TOP-REAL
n, E being Subset of I(01) st (ex p1, p2 being Point of I[01] st p1 < p2 & E =
  [. p1,p2 .]) & I(01)|E, (TOP-REAL n)|C are_homeomorphic holds ex s1, s2 being
  Point of TOP-REAL n st C is_an_arc_of s1,s2;

theorem :: BORSUK_4:55
  for Dp being non empty Subset of TOP-REAL 2, f being Function of
  (TOP-REAL 2) | Dp, I(01), C being non empty Subset of TOP-REAL 2 st f is
being_homeomorphism & C c= Dp & (ex p1, p2 being Point of I[01] st p1 < p2 & f
.:C = [. p1,p2 .]) holds ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of
  s1,s2;

theorem :: BORSUK_4:56
  for D being Simple_closed_curve, C being non empty compact connected
  Subset of TOP-REAL 2 st C c= D holds C = D or (ex p1, p2 being Point of
TOP-REAL 2 st C is_an_arc_of p1,p2) or ex p being Point of TOP-REAL 2 st C = {p
  };

begin :: Addenda

theorem :: BORSUK_4:57
  for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex D being non empty closed_interval Subset of REAL
 st C c= D & D c= ].0,1.[ &
 lower_bound C = lower_bound D & upper_bound C = upper_bound D;

theorem :: BORSUK_4:58
  for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex p1, p2 being Point of I[01] st p1 <= p2 & C c= [. p1, p2 .] & [.p1,p2
  .] c= ]. 0, 1 .[;

theorem :: BORSUK_4:59
  for D being Simple_closed_curve, C being closed Subset of TOP-REAL 2
st C c< D ex p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2 st B
  is_an_arc_of p1,p2 & C c= B & B c= D;