The abstract of the Mizar article:

On the Decompositions of Intervals and Simple Closed Curves

by

Adam Grabowski

Received August 7, 2002

MML identifier: BORSUK_4

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, TOPREAL1, EUCLID, ARYTM_1, PRE_TOPC, COMPTS_1, SEQ_1,
      TOPREAL2, RELAT_2, BORSUK_1, SUBSET_1, RCOMP_1, TOPS_2, TOPMETR,
      CONNSP_1, ARYTM_3, SQUARE_1, RELAT_1, ORDINAL2, LATTICES, T_0TOPSP,
      SEQ_2, INTEGRA1, REALSET1, FUNCT_1, BORSUK_4, PARTFUN1, TREAL_1, FUNCT_4,
      ARYTM, JORDAN1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, REALSET1, FUNCT_2,
      STRUCT_0, PRE_TOPC, COMPTS_1, FUNCT_4, RCOMP_1, EUCLID, TOPREAL1,
      TOPREAL2, SEQ_4, T_0TOPSP, TREAL_1, CONNSP_1, BORSUK_1, BORSUK_3, TSEP_1,
      RCOMP_2, JORDAN1, TOPMETR, PSCOMP_1, INTEGRA1, TOPS_2;
 constructors REALSET1, JORDAN2C, TOPS_2, TOPREAL2, TOPREAL1, CONNSP_1,
      RCOMP_2, PSCOMP_1, INTEGRA1, TMAP_1, BORSUK_3, COMPTS_1, YELLOW_8,
      PARTFUN1, LIMFUNC1, SPPOL_1, TOPGRP_1, TREAL_1, DOMAIN_1, XCMPLX_0,
      MEMBERED, JORDAN1;
 clusters XREAL_0, RELSET_1, REVROT_1, TOPREAL6, STRUCT_0, PRE_TOPC, BORSUK_2,
      REALSET1, INTEGRA1, TEX_1, TEX_2, JORDAN1B, YELLOW13, EUCLID, MEMBERED,
      ZFMISC_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

definition
  cluster -> non trivial Simple_closed_curve;
end;

definition let T be non empty TopSpace;
  cluster non empty compact connected Subset of T;
end;

definition
  cluster -> real Element of I[01];
end;

theorem :: BORSUK_4:1
  for X being non empty set,
      A, B being non empty Subset of X st A c< B holds
   ex p being Element of X st p in B & A c= B \ {p};

theorem :: BORSUK_4:2
  for X being non empty set,
      A being non empty Subset of X holds
   A is trivial iff ex x being Element of X st A = {x};

definition let T be non trivial 1-sorted;
  cluster non trivial Subset of T;
end;

theorem :: BORSUK_4:3
    for X being non trivial set,
      p being set
   ex q being Element of X st q <> p;

definition let X be non trivial set;
 cluster non trivial Subset of X;
end;

theorem :: BORSUK_4:4
  for T being non trivial set,
      X being non trivial Subset of T,
      p being set
    ex q being Element of T st q in X & q <> p;

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 } holds
     f +* g is one-to-one;

theorem :: BORSUK_4:6
  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:7
  for n being Nat,
      A being non empty 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:8
    for n being Nat,
      a,b being Point of TOP-REAL n holds LSeg (a,b) is convex;

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

theorem :: BORSUK_4:10
  for x being set, a, b being real number st a <= b &
    x in [. a, b .] holds x in ]. a, b .[ or x = a or x = b;

theorem :: BORSUK_4:11
  for a, b, c, d being real number st
    ].a,b.[ meets [.c,d.] holds b > c;

theorem :: BORSUK_4:12
  for a, b, c, d being real number st
    b <= c holds [. a, b .] misses ]. c, d .[;

theorem :: BORSUK_4:13
  for a, b, c, d being real number st
    b <= c holds ]. a, b .[ misses [. c, d .];

theorem :: BORSUK_4:14
    for a, b, c, d being real number st a < b &
    [.a,b.] c= [.c,d.] holds c <= a & b <= d;

theorem :: BORSUK_4:15
  for a, b, c, d being real number st a < b &
    ].a,b.[ c= [.c,d.] holds c <= a & b <= d;

theorem :: BORSUK_4:16
    for a, b, c, d being real number st a < b &
    ].a,b.[ c= [.c,d.] holds [.a,b.] c= [.c,d.];

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

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

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

theorem :: BORSUK_4:20
  for a, b being real number st a <> b holds Cl ].a,b.] = [.a,b.];

theorem :: BORSUK_4:21
  for a, b being real number st a <> b holds Cl [.a,b.[ = [.a,b.];

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

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

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

theorem :: BORSUK_4:25
    for a,b being real number st a < b holds
   [.a,b.] <> ].a,b.];

theorem :: BORSUK_4:26
  for a, b being real number holds
    [.a,b.[ misses {b} & ].a,b.] misses {a};

theorem :: BORSUK_4:27
  for a, b being real number st a <= b holds
    [. a, b .] \ { a } = ]. a, b .];

theorem :: BORSUK_4:28
  for a, b being real number st a <= b holds
    [. a, b .] \ { b } = [. a, b .[;

theorem :: BORSUK_4:29
  for a, b, c being real number st a < b & b < c holds
    ]. a, b .] /\ [. b, c .[ = { b };

theorem :: BORSUK_4:30
  for a, b, c being real number holds
    [. a, b .[ misses [. b, c .] & [. a, b .] misses ]. b, c .];

theorem :: BORSUK_4:31
  for a, b, c being real number st a <= b & b <= c holds
   [.a,c.] \ {b} = [.a,b.[ \/ ].b,c.];

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

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

theorem :: BORSUK_4:34
  for a, b being real number st a <= b holds
    [. a, b .] = [. a, b .[ \/ { b };

theorem :: BORSUK_4:35
  for a, b being real number st a <= b holds
    [. a, b .] = { a } \/ ]. a, b .];

theorem :: BORSUK_4:36
  for a, b, c, d being real number st a <= b & b < c & c <= d holds
    [. a, d .] = [. a, b .] \/ ]. b, c .[ \/ [. c, d .];

theorem :: BORSUK_4:37
  for a, b, c, d being real number st a <= b & b < c & c <= d holds
    [. a, d .] \ ([. a, b .] \/ [. c, d .]) = ]. b, c .[;

theorem :: BORSUK_4:38
  for a, b, c being real number st a < b & b < c holds
    ]. a, b .] \/ ]. b, c .[ = ]. a, c .[;

theorem :: BORSUK_4:39
  for a, b, c being real number st a < b & b < c holds
    [. b, c .[ c= ]. a, c .[;

theorem :: BORSUK_4:40
  for a, b, c being real number st a < b & b < c holds
    ]. a, b .] \/ [. b, c .[ = ]. a, c .[;

theorem :: BORSUK_4:41
  for a, b, c being real number st a < b & b < c holds
    ]. a, c .[ \ ]. a, b .] = ]. b, c .[;

theorem :: BORSUK_4:42
  for a, b, c being real number st a < b & b < c holds
    ]. a, c .[ \ [. b, c .[ = ]. a, b .[;

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

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

begin :: Decompositions of Intervals

theorem :: BORSUK_4:45
    for p being real number holds
   {p} is closed-interval Subset of REAL;

theorem :: BORSUK_4:46
  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:47
  for A being non empty connected Subset of I[01],
      a, b being real number st a in A & b in A holds
   [.a,b.] c= A;

theorem :: BORSUK_4:48
  for a, b being real number,
      A being Subset of I[01] st a <= b & A = [.a,b.] holds
    A is closed;

theorem :: BORSUK_4:49
  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:50
  for X being Subset of I[01],
      X' being Subset of REAL st X' = X holds
    X' is bounded_above bounded_below;

theorem :: BORSUK_4:51
  for X being Subset of I[01],
      X' being Subset of REAL,
      x being real number st x in X' & X' = X holds
    inf X' <= x & x <= sup X';

theorem :: BORSUK_4:52
  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:53
  for C being closed-interval Subset of REAL holds inf C <= sup C;

theorem :: BORSUK_4:54
  for C being non empty compact connected Subset of I[01],
      C' being Subset of REAL st C = C' & [. inf C', sup C' .] c= C' holds
   [. inf C', sup C' .] = C';

theorem :: BORSUK_4:55
  for C being non empty compact connected Subset of I[01] holds
    C is closed-interval Subset of REAL;

theorem :: BORSUK_4:56
  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 non empty SubSpace of I[01] means
:: BORSUK_4:def 1
    the carrier of it = ]. 0,1 .[;
end;

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

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

theorem :: BORSUK_4:59
  I(01) is open SubSpace of I[01];

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

theorem :: BORSUK_4:61
  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:62
  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:63
    for D being Simple_closed_curve holds
    (TOP-REAL 2) | R^2-unit_square, (TOP-REAL 2) | D are_homeomorphic;

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

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

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

theorem :: BORSUK_4:67
  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:68
  for A being non empty Subset of TOP-REAL 2,
      p, q being Point of TOP-REAL 2,
      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 map of I[01]|E, (TOP-REAL 2)|A st
    E = [. a, b .] & f is_homeomorphism & f.a = p & f.b = q;

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

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

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

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

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

theorem :: BORSUK_4:74
  for A being non empty Subset of TOP-REAL 2,
      p, q being Point of TOP-REAL 2,
      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 map of I(01)|E, (TOP-REAL 2)|(A \ {p}) st
    E = ]. a, b .] & f is_homeomorphism & f.b = q;

theorem :: BORSUK_4:75
  for A being non empty Subset of TOP-REAL 2,
      p, q being Point of TOP-REAL 2,
      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 map of I(01)|E, (TOP-REAL 2)|(A \ {q}) st
    E = [. a, b .[ & f is_homeomorphism & f.a = p;

theorem :: BORSUK_4:76
  for A, B being non empty Subset of TOP-REAL 2,
      p, q being Point of TOP-REAL 2 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 2) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic;

theorem :: BORSUK_4:77
  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:78
    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:79
  for C being non empty Subset of TOP-REAL 2,
      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 2)|C are_homeomorphic holds
  ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of s1,s2;

theorem :: BORSUK_4:80
  for Dp being non empty Subset of TOP-REAL 2,
      f being map of (TOP-REAL 2) | Dp, I(01),
      C being non empty Subset of TOP-REAL 2 st
    f is_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:81
    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});