The abstract of the Mizar article:

On the Subcontinua of a Real Line

by

Adam Grabowski

Received June 12, 2003

MML identifier: BORSUK_5

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, ARYTM_1, PRE_TOPC, COMPTS_1, SEQ_1, RELAT_2, BORSUK_1,
      SUBSET_1, RCOMP_1, TOPMETR, CONNSP_1, ARYTM_3, SQUARE_1, RELAT_1,
      ORDINAL2, LATTICES, SEQ_2, INTEGRA1, FUNCT_1, TREAL_1, ARYTM, LIMFUNC1,
      BORSUK_2, PCOMPS_1, GRAPH_1, INCPROJ, CARD_1, SETFAM_1, RAT_1, METRIC_1,
      FINSET_1, ABSVALUE, IRRAT_1, POWER, INT_1, BORSUK_5, XREAL_0;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, ENUMSET1, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, INT_1,
      PRE_TOPC, COMPTS_1, RCOMP_1, SEQ_4, TREAL_1, RCOMP_2, CONNSP_1, BORSUK_2,
      CARD_1, TOPMETR, PSCOMP_1, INTEGRA1, LIMFUNC1, IRRAT_1, FINSET_1,
      ABSVALUE, INCPROJ, RAT_1, METRIC_1, PCOMPS_1, NECKLACE;
 constructors TOPS_2, CONNSP_1, RCOMP_2, PSCOMP_1, INTEGRA1, BORSUK_3,
      COMPTS_1, YELLOW_8, PARTFUN1, LIMFUNC1, TREAL_1, POWER, PROB_1, BORSUK_2,
      ENUMSET1, NAT_1, INCPROJ, URYSOHN1, RAT_1, NECKLACE, MEMBERED;
 clusters XREAL_0, RELSET_1, TOPREAL6, STRUCT_0, PRE_TOPC, BORSUK_2, INTEGRA1,
      YELLOW13, TOPS_1, JORDAN6, BORSUK_4, FINSET_1, RAT_1, METRIC_1, INT_1,
      MEMBERED, ZFMISC_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

canceled;

theorem :: BORSUK_5:2
  for A, B, a being set st
    A c= B & B c= A \/ {a} holds
      A \/ {a} = B or A = B;

theorem :: BORSUK_5:3
   for x1, x2, x3, x4, x5, x6 being set holds
    { x1, x2, x3, x4, x5, x6 } = { x1, x3, x6 } \/ { x2, x4, x5 };

 reserve x1, x2, x3, x4, x5, x6, x7 for set;

definition let x1, x2, x3, x4, x5, x6 be set;
  pred x1, x2, x3, x4, x5, x6 are_mutually_different means
:: BORSUK_5:def 1
    x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 &
    x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 &
    x3 <> x4 & x3 <> x5 & x3 <> x6 &
    x4 <> x5 & x4 <> x6 &
    x5 <> x6;
end;

definition let x1, x2, x3, x4, x5, x6, x7 be set;
  pred x1, x2, x3, x4, x5, x6, x7 are_mutually_different means
:: BORSUK_5:def 2
    x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 &
    x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 &
    x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 &
    x4 <> x5 & x4 <> x6 & x4 <> x7 &
    x5 <> x6 & x5 <> x7 &
    x6 <> x7;
end;

theorem :: BORSUK_5:4
  for x1, x2, x3, x4, x5, x6 being set st
    x1, x2, x3, x4, x5, x6 are_mutually_different holds
      card {x1, x2, x3, x4, x5, x6} = 6;

theorem :: BORSUK_5:5
   for x1, x2, x3, x4, x5, x6, x7 being set st
    x1, x2, x3, x4, x5, x6, x7 are_mutually_different holds
      card {x1, x2, x3, x4, x5, x6, x7} = 7;

theorem :: BORSUK_5:6
  { x1, x2, x3 } misses { x4, x5, x6 } implies
    x1 <> x4 & x1 <> x5 & x1 <> x6 &
    x2 <> x4 & x2 <> x5 & x2 <> x6 &
    x3 <> x4 & x3 <> x5 & x3 <> x6;

theorem :: BORSUK_5:7
   x1, x2, x3 are_mutually_different &
   x4, x5, x6 are_mutually_different &
    { x1, x2, x3 } misses { x4, x5, x6 } implies
      x1, x2, x3, x4, x5, x6 are_mutually_different;

theorem :: BORSUK_5:8
   x1, x2, x3, x4, x5, x6 are_mutually_different &
    { x1, x2, x3, x4, x5, x6 } misses { x7 } implies
      x1, x2, x3, x4, x5, x6, x7 are_mutually_different;

theorem :: BORSUK_5:9
   x1, x2, x3, x4, x5, x6, x7 are_mutually_different implies
    x7, x1, x2, x3, x4, x5, x6 are_mutually_different;

theorem :: BORSUK_5:10
   x1, x2, x3, x4, x5, x6, x7 are_mutually_different implies
    x1, x2, x5, x3, x6, x7, x4 are_mutually_different;

theorem :: BORSUK_5:11
  for T being non empty TopSpace,
      a, b being Point of T st
    (ex f being map of I[01], T st f is continuous & f.0 = a & f.1 = b) holds
     ex g being map of I[01], T st g is continuous & g.0 = b & g.1 = a;

definition
  cluster R^1 -> arcwise_connected;
end;

definition
  cluster connected non empty TopSpace;
end;

begin :: Intervals

theorem :: BORSUK_5:12
   for A being Subset of REAL holds
    A is Subset of R^1;

theorem :: BORSUK_5:13
  [#]R^1 = REAL;

definition let a be real number;
  redefine func left_closed_halfline a; :: LIMFUNC1
  synonym ].-infty, a .];
  redefine func left_open_halfline a;
  synonym ].-infty, a .[;
  redefine func right_closed_halfline a;
  synonym [. a,+infty.[;
  redefine func right_open_halfline a;
  synonym ]. a,+infty.[;
end;

theorem :: BORSUK_5:14
  for a, b being real number holds
    a in ]. b,+infty.[ iff a > b;

theorem :: BORSUK_5:15
  for a, b being real number holds
    a in [. b,+infty.[ iff a >= b;

theorem :: BORSUK_5:16
  for a, b being real number holds
    a in ].-infty, b .] iff a <= b;

theorem :: BORSUK_5:17
  for a, b being real number holds
    a in ].-infty, b .[ iff a < b;

theorem :: BORSUK_5:18
  for a being real number holds
    REAL \ {a} = ].-infty, a .[ \/ ]. a,+infty.[;

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

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

theorem :: BORSUK_5:21
   for A, B being Subset of R^1,
      a, b, c, d being real number st a < b & b <= c & c < d &
    A = [. a, b .[ & B = ]. c, d .] holds
  A, B are_separated;

theorem :: BORSUK_5:22
  for a being real number holds
    REAL \ ].-infty, a .[ = [. a,+infty.[;

theorem :: BORSUK_5:23
  for a being real number holds
    REAL \ ].-infty, a .] = ]. a,+infty.[;

theorem :: BORSUK_5:24
   for a being real number holds
    REAL \ ]. a,+infty.[ = ].-infty, a .];

theorem :: BORSUK_5:25
  for a being real number holds
    REAL \ [. a,+infty.[ = ].-infty, a .[;

theorem :: BORSUK_5:26
  for a being real number holds
    ].-infty, a .] misses ]. a,+infty.[;

theorem :: BORSUK_5:27
  for a being real number holds
    ].-infty, a .[ misses [. a,+infty.[;

theorem :: BORSUK_5:28
  for a, b, c being real number st
    a <= c & c <= b holds [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[;

theorem :: BORSUK_5:29
  for a, b, c being real number st
    a <= c & c <= b holds ].-infty, c .] \/ [. a, b .] = ].-infty, b .];

theorem :: BORSUK_5:30
  for T being 1-sorted,
      A being Subset of T holds
    { A } is Subset-Family of T;

theorem :: BORSUK_5:31
   for T being 1-sorted,
      A, B being Subset of T holds
    { A, B } is Subset-Family of T;

theorem :: BORSUK_5:32
   for T being 1-sorted,
      A, B, C being Subset of T holds
    { A, B, C } is Subset-Family of T;

definition
  cluster -> real Element of RAT;
end;

definition
  cluster -> real Element of RealSpace;
end;

theorem :: BORSUK_5:33
  for A being Subset of R^1,
      p being Point of RealSpace holds
    p in Cl A iff
      for r being real number st r > 0 holds Ball (p, r) meets A;

theorem :: BORSUK_5:34
  for p, q being Element of RealSpace st q >= p holds
    dist (p, q) = q - p;

theorem :: BORSUK_5:35
  for A being Subset of R^1 st A = RAT holds
    Cl A = the carrier of R^1;

theorem :: BORSUK_5:36
  for A being Subset of R^1,
      a, b being real number st
    A = ]. a, b .[ & a <> b holds
      Cl A = [. a, b .];

begin :: Rational and Irrational Numbers

definition
  cluster number_e -> irrational;
end;

definition
  func IRRAT -> Subset of REAL equals
:: BORSUK_5:def 3
    REAL \ RAT;
end;

definition let a, b be real number;
  func RAT (a, b) -> Subset of REAL equals
:: BORSUK_5:def 4
    RAT /\ ]. a, b .[;
  func IRRAT (a, b) -> Subset of REAL equals
:: BORSUK_5:def 5
    IRRAT /\ ]. a, b .[;
end;

theorem :: BORSUK_5:37
  for x being real number holds
    x is irrational iff x in IRRAT;

definition
  cluster irrational (real number);
end;

definition
  cluster IRRAT -> non empty;
end;

theorem :: BORSUK_5:38
  for a being rational number, b being irrational (real number) holds
    a + b is irrational;

theorem :: BORSUK_5:39
  for a being irrational (real number) holds -a is irrational;

theorem :: BORSUK_5:40
  for a being rational number, b being irrational (real number) holds
    a - b is irrational;

theorem :: BORSUK_5:41
  for a being rational number, b being irrational (real number) holds
    b - a is irrational;

theorem :: BORSUK_5:42
  for a being rational number, b being irrational (real number) st
    a <> 0 holds a * b is irrational;

theorem :: BORSUK_5:43
  for a being rational number, b being irrational (real number)
    st a <> 0 holds b / a is irrational;

definition
  cluster irrational -> non zero (real number);
end;

theorem :: BORSUK_5:44
  for a being rational number, b being irrational (real number)
    st a <> 0 holds a / b is irrational;

theorem :: BORSUK_5:45
  for r being irrational (real number) holds frac r is irrational;

definition let r be irrational (real number);
  cluster frac r -> irrational;
end;

definition let a be irrational (real number);
  cluster -a -> irrational;
end;

definition let a be rational number, b be irrational (real number);
  cluster a + b -> irrational;
  cluster b + a -> irrational;
  cluster a - b -> irrational;
  cluster b - a -> irrational;
end;

definition
  cluster non zero (rational number);
end;

definition let a be non zero (rational number), b be irrational (real number);
  cluster a * b -> irrational;
  cluster b * a -> irrational;
  cluster a / b -> irrational;
  cluster b / a -> irrational;
end;

theorem :: BORSUK_5:46
   for r being irrational (real number) holds 0 < frac r;

theorem :: BORSUK_5:47
  for a, b being real number st a < b
   ex p1, p2 being rational number st
     a < p1 & p1 < p2 & p2 < b;

theorem :: BORSUK_5:48
  for s1, s3, s4, l being real number holds
    s1 <= s3 & s1 < s4 & 0 < l & l < 1 implies s1 < (1-l)*s3+l*s4;

theorem :: BORSUK_5:49
  for s1, s3, s4, l being real number holds
    s3 < s1 & s4 <= s1 & 0 < l & l < 1 implies (1-l)*s3+l*s4 < s1;

theorem :: BORSUK_5:50
  for a, b being real number st a < b
    ex p being irrational (real number) st a < p & p < b;

theorem :: BORSUK_5:51
  for A being Subset of R^1 st A = IRRAT holds
   Cl A = the carrier of R^1;

theorem :: BORSUK_5:52
  for a, b, c being real number st a < b holds
    c in RAT (a,b) iff c is rational & a < c & c < b;

theorem :: BORSUK_5:53
  for a, b, c being real number st a < b holds
    c in IRRAT (a,b) iff c is irrational & a < c & c < b;

theorem :: BORSUK_5:54
  for A being Subset of R^1,
      a, b being real number st a < b & A = RAT (a, b) holds
    Cl A = [. a, b .];

theorem :: BORSUK_5:55
  for A being Subset of R^1,
      a, b being real number st a < b & A = IRRAT (a, b) holds
    Cl A = [. a, b .];

theorem :: BORSUK_5:56
  for T being connected TopSpace,
      A being closed open Subset of T holds
    A = {} or A = [#]T;

theorem :: BORSUK_5:57
  for A being Subset of R^1 st A is closed open holds
    A = {} or A = REAL;

begin :: Topological Properties of Intervals

theorem :: BORSUK_5:58
  for A being Subset of R^1,
      a, b being real number st
    A = [. a, b .[ & a <> b holds
      Cl A = [. a, b .];

theorem :: BORSUK_5:59
  for A being Subset of R^1,
      a, b being real number st
    A = ]. a, b .] & a <> b holds
      Cl A = [. a, b .];

theorem :: BORSUK_5:60
   for A being Subset of R^1,
      a, b, c being real number st
    A = [. a, b .[ \/ ]. b, c .] & a < b & b < c holds
      Cl A = [. a, c .];

theorem :: BORSUK_5:61
  for A being Subset of R^1,
      a being real number st A = {a} holds Cl A = {a};

theorem :: BORSUK_5:62
  for A being Subset of REAL, B being Subset of R^1 st A = B holds
      A is open iff B is open;

theorem :: BORSUK_5:63
  for A being Subset of R^1,
      a being real number st
    A = ]. a,+infty.[ holds A is open;

theorem :: BORSUK_5:64
  for A being Subset of R^1,
      a being real number st
    A = ].-infty,a .[ holds A is open;

theorem :: BORSUK_5:65
  for A being Subset of R^1,
      a being real number st
    A = ].-infty,a.] holds A is closed;

theorem :: BORSUK_5:66
  for A being Subset of R^1,
      a being real number st
    A = [. a,+infty.[ holds A is closed;

theorem :: BORSUK_5:67
  for a being real number holds
    [. a,+infty.[ = {a} \/ ]. a,+infty.[;

theorem :: BORSUK_5:68
  for a being real number holds
    ].-infty,a.] = {a} \/ ].-infty,a.[;

theorem :: BORSUK_5:69
  for a being real number holds
    ]. a,+infty.[ c= [. a,+infty.[;

theorem :: BORSUK_5:70
  for a being real number holds
    ].-infty,a .[ c= ].-infty,a .];

definition let a be real number;
  cluster ]. a,+infty.[ -> non empty;
  cluster ].-infty,a .] -> non empty;
  cluster ].-infty,a .[ -> non empty;
  cluster [. a,+infty.[ -> non empty;
end;

theorem :: BORSUK_5:71
  for a being real number holds
    ]. a,+infty.[ <> REAL;

theorem :: BORSUK_5:72
   for a being real number holds
    [. a,+infty.[ <> REAL;

theorem :: BORSUK_5:73
   for a being real number holds
    ].-infty, a .] <> REAL;

theorem :: BORSUK_5:74
  for a being real number holds
    ].-infty, a .[ <> REAL;

theorem :: BORSUK_5:75
  for A being Subset of R^1,
      a being real number st
    A = ]. a,+infty.[ holds Cl A = [. a,+infty.[;

theorem :: BORSUK_5:76
   for a being real number holds
    Cl ]. a,+infty.[ = [. a,+infty.[;

theorem :: BORSUK_5:77
  for A being Subset of R^1,
      a being real number st
     A = ].-infty, a .[ holds Cl A = ].-infty, a .];

theorem :: BORSUK_5:78
    for a being real number holds
    Cl ].-infty, a .[ = ].-infty, a .];

theorem :: BORSUK_5:79
  for A, B being Subset of R^1,
      b being real number st
    A = ].-infty, b .[ & B = ]. b,+infty.[ holds A, B are_separated;

theorem :: BORSUK_5:80
    for A being Subset of R^1,
      a, b being real number st a < b &
    A = [. a, b .[ \/ ]. b,+infty.[ holds Cl A = [. a,+infty.[;

theorem :: BORSUK_5:81
  for A being Subset of R^1,
      a, b being real number st a < b &
    A = ]. a, b .[ \/ ]. b,+infty.[ holds Cl A = [. a,+infty.[;

theorem :: BORSUK_5:82
   for A being Subset of R^1,
      a, b, c being real number st a < b & b < c &
    A = RAT (a,b) \/ ]. b, c .[ \/ ]. c,+infty.[ holds
      Cl A = [. a,+infty.[;

theorem :: BORSUK_5:83
   for A being Subset of R^1 holds
    A` = REAL \ A;

theorem :: BORSUK_5:84
  for a, b being real number st a < b holds
    IRRAT (a, b) misses RAT (a, b);

theorem :: BORSUK_5:85
  for a, b being real number st a < b holds
    REAL \ RAT (a, b) = ].-infty,a.] \/ IRRAT (a, b) \/ [.b,+infty.[;

theorem :: BORSUK_5:86
  for a, b, c being real number st a <= b & b < c holds
    not a in ]. b, c .[ \/ ]. c,+infty.[;

theorem :: BORSUK_5:87
  for a, b being real number st a < b holds
    not b in ]. a, b .[ \/ ]. b,+infty.[;

theorem :: BORSUK_5:88
  for a, b being real number st a < b holds
    [.a,+infty.[ \ (]. a, b .[ \/ ]. b,+infty.[) = {a} \/ {b};

theorem :: BORSUK_5:89
   for A being Subset of R^1 st
    A = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[ holds
      A` = ].-infty,2 .] \/ IRRAT(2,3) \/ {3} \/ {4};

theorem :: BORSUK_5:90
   for A being Subset of R^1,
      a being real number st A = {a} holds
   A` = ].-infty, a .[ \/ ]. a,+infty.[;

theorem :: BORSUK_5:91
  for a, b being real number st a < b holds
    ]. a,+infty.[ /\ ].-infty, b .] = ]. a, b .];

theorem :: BORSUK_5:92
   (].-infty, 1 .[ \/ ]. 1,+infty.[) /\
    (].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) =
      ].-infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4};

theorem :: BORSUK_5:93
  for a, b being real number st a <= b holds
    ].-infty,b.[ \ {a} = ].-infty, a .[ \/ ]. a, b .[;

theorem :: BORSUK_5:94
  for a, b being real number st a <= b holds
    ]. a,+infty.[ \ {b} = ]. a, b .[ \/ ]. b,+infty.[;

theorem :: BORSUK_5:95
   for A being Subset of R^1,
      a, b being real number st a <= b &
    A = {a} \/ [. b,+infty.[ holds
    A` = ].-infty, a .[ \/ ]. a, b .[;

theorem :: BORSUK_5:96
   for A being Subset of R^1,
      a, b being real number st a < b &
     A = ].-infty, a .[ \/ ]. a, b .[ holds Cl A = ].-infty, b .];

theorem :: BORSUK_5:97
  for A being Subset of R^1,
      a, b being real number st a < b &
     A = ].-infty, a .[ \/ ]. a, b .] holds Cl A = ].-infty, b .];

theorem :: BORSUK_5:98
   for A being Subset of R^1,
      a being real number st
     A = ].-infty, a .] holds A` = ]. a ,+infty.[;

theorem :: BORSUK_5:99
   for A being Subset of R^1,
      a being real number st
     A = [. a ,+infty.[ holds A` = ].-infty, a .[;

theorem :: BORSUK_5:100
  for A being Subset of R^1,
      a, b, c being real number st a < b & b < c &
       A = ].-infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} holds
    Cl A = ].-infty, c .];

theorem :: BORSUK_5:101
   for A being Subset of R^1,
      a, b, c, d being real number st a < b & b < c &
       A = ].-infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} \/ {d} holds
    Cl A = ].-infty, c .] \/ {d};

theorem :: BORSUK_5:102
   for A being Subset of R^1,
      a, b being real number st a <= b &
    A = ].-infty, a .] \/ {b} holds
    A` = ]. a, b .[ \/ ]. b,+infty.[;

theorem :: BORSUK_5:103
   for a, b being real number holds
    [. a,+infty.[ \/ {b} <> REAL;

theorem :: BORSUK_5:104
   for a, b being real number holds
    ].-infty, a .] \/ {b} <> REAL;

theorem :: BORSUK_5:105
   for TS being TopStruct,
      A, B being Subset of TS st A <> B holds A` <> B`;

theorem :: BORSUK_5:106
   for A being Subset of R^1 st REAL = A` holds A = {};

begin :: Subcontinua of a real line

definition
  cluster I[01] -> arcwise_connected;
end;

theorem :: BORSUK_5:107
  for X being compact Subset of R^1,
      X' being Subset of REAL st X' = X holds
    X' is bounded_above bounded_below;

theorem :: BORSUK_5:108
  for X being compact Subset of R^1,
      X' being Subset of REAL,
      x being real number st x in X' & X' = X holds
    inf X' <= x & x <= sup X';

theorem :: BORSUK_5:109
  for C being non empty compact connected Subset of R^1,
      C' being Subset of REAL st C = C' & [. inf C', sup C' .] c= C' holds
   [. inf C', sup C' .] = C';

theorem :: BORSUK_5:110  :: TOPREAL5:9
  for A being connected Subset of R^1,
      a, b, c being real number st
    a <= b & b <= c & a in A & c in A holds b in A;

theorem :: BORSUK_5:111
  for A being connected Subset of R^1,
      a, b being real number st a in A & b in A holds
   [.a,b.] c= A;

theorem :: BORSUK_5:112
  for X being non empty compact connected Subset of R^1 holds
    X is non empty closed-interval Subset of REAL;

theorem :: BORSUK_5:113
   for A being non empty compact connected Subset of R^1 holds
   ex a, b being real number st a <= b & A = [. a, b .];

begin :: Sets with Proper Subsets Only

definition let TS be TopStruct; let F be Subset-Family of TS;
  attr F is with_proper_subsets means
:: BORSUK_5:def 6
    not the carrier of TS in F;
end;

theorem :: BORSUK_5:114
   for TS being TopStruct,
      F, G being Subset-Family of TS st
    F is with_proper_subsets & G c= F holds
    G is with_proper_subsets;

definition let TS be non empty TopStruct;
  cluster with_proper_subsets Subset-Family of TS;
end;

theorem :: BORSUK_5:115
   for TS being non empty TopStruct,
      A, B being with_proper_subsets Subset-Family of TS holds
    A \/ B is with_proper_subsets;

definition let T be TopStruct, F be Subset-Family of T;
  attr F is open means
:: BORSUK_5:def 7  :: TOPS_2:def 1
      for P being Subset of T holds P in F implies P is open;
  attr F is closed means
:: BORSUK_5:def 8  :: TOPS_2:def 2
      for P being Subset of T holds P in F implies P is closed;
end;

definition let T be TopSpace;
  cluster open closed non empty Subset-Family of T;
end;