:: Properties of Connected Subsets of the Real Line
::  by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-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, XBOOLE_0, SUBSET_1, MEMBERED, PRE_TOPC, METRIC_1,
      STRUCT_0, XXREAL_2, RCOMP_1, TARSKI, ORDINAL2, SEQ_4, TOPMETR, XXREAL_1,
      RELAT_2, CARD_1, ARYTM_3, XXREAL_0, REAL_1, ARYTM_1, LIMFUNC1, ZFMISC_1,
      TOPS_1, RELAT_1, SETFAM_1, FINSET_1, ORDERS_1, WELLORD1, FINSEQ_1,
      PARTFUN1, WELLORD2, FUNCT_1, NAT_1, RCOMP_3, MEASURE5, FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, SETFAM_1, FUNCT_1,
      RELSET_1, PARTFUN1, FINSET_1, WELLORD1, ORDERS_1, WELLORD2, RELAT_2,
      CARD_1, MEMBERED, NUMBERS, XCMPLX_0, XXREAL_0, MEASURE6, XREAL_0, NAT_1,
      NAT_D, LIMFUNC1, XXREAL_1, XXREAL_2, SEQM_3, FINSEQ_1, VALUED_0,
      VALUED_1, FUNCT_2, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1,
      TOPS_2, COMPTS_1, CONNSP_1, TOPMETR, TOPALG_2, TOPREALB;
 constructors WELLORD1, WELLORD2, ORDERS_1, PROB_1, LIMFUNC1, BINARITH, TOPS_1,
      CONNSP_1, COMPTS_1, MEASURE6, TOPREALB, BORSUK_6, NAT_D, SEQ_4, FUNCT_2,
      BINOP_1;
 registrations SUBSET_1, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, FINSEQ_1, RCOMP_1, FCONT_3, STRUCT_0, PRE_TOPC, TOPS_1,
      METRIC_1, TOPMETR, MEASURE6, BORSUK_2, SPRECT_1, TOPREAL6, TOPALG_2,
      TOPREALB, FINSET_1, VALUED_0, XXREAL_2, CARD_1, XXREAL_1, SEQ_4,
      WELLORD2, RELSET_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Preliminaries

registration
  let X be non empty set;
  cluster [#]X -> non empty;
end;

registration
  cluster -> real-membered for SubSpace of RealSpace;
end;

theorem :: RCOMP_3:1
  for X being non empty bounded_below real-membered set, Y being
  closed Subset of REAL st X c= Y holds lower_bound X in Y;

theorem :: RCOMP_3:2
  for X being non empty bounded_above real-membered set, Y being
  closed Subset of REAL st X c= Y holds upper_bound X in Y;

theorem :: RCOMP_3:3
  for X, Y being Subset of REAL holds Cl(X \/ Y) = Cl X \/ Cl Y;

begin :: Intervals

reserve a, b, r, s for Real;

registration
  let r be Real, s be ExtReal;
  cluster [.r,s.[ -> bounded_below;
  cluster ].s,r.] -> bounded_above;
end;

registration
  let r, s;
  cluster [.r,s.[ -> real-bounded;
  cluster ].r,s.] -> real-bounded;
  cluster ].r,s.[ -> real-bounded;
end;

registration
  cluster open real-bounded interval non empty for Subset of REAL;
end;

theorem :: RCOMP_3:4
  r < s implies lower_bound [.r,s.[ = r;

theorem :: RCOMP_3:5
  r < s implies upper_bound [.r,s.[ = s;

theorem :: RCOMP_3:6
  r < s implies lower_bound ].r,s.] = r;

theorem :: RCOMP_3:7
  r < s implies upper_bound ].r,s.] = s;

begin :: Halflines

theorem :: RCOMP_3:8
  a <= b implies [.a,b.] /\ (left_closed_halfline(a) \/
  right_closed_halfline(b)) = {a,b};

registration
  let a;
  cluster left_closed_halfline(a) -> non bounded_below bounded_above interval;
  cluster left_open_halfline(a) -> non bounded_below bounded_above interval;
  cluster right_closed_halfline(a) -> bounded_below non bounded_above interval;
  cluster right_open_halfline(a) -> bounded_below non bounded_above interval;
end;

theorem :: RCOMP_3:9
  upper_bound left_closed_halfline(a) = a;

theorem :: RCOMP_3:10
  upper_bound left_open_halfline(a) = a;

theorem :: RCOMP_3:11
  lower_bound right_closed_halfline(a) = a;

theorem :: RCOMP_3:12
  lower_bound right_open_halfline(a) = a;

begin :: Connectedness

registration
  cluster [#]REAL -> interval non bounded_below non bounded_above;
end;

theorem :: RCOMP_3:13
  for X being real-bounded interval Subset of REAL st lower_bound X in
  X & upper_bound X in X holds X = [.lower_bound X,upper_bound X.];

theorem :: RCOMP_3:14
  for X being real-bounded Subset of REAL st not lower_bound X in X
  holds X c= ].lower_bound X,upper_bound X.];

theorem :: RCOMP_3:15
  for X being real-bounded interval Subset of REAL st not lower_bound
  X in X & upper_bound X in X holds X = ].lower_bound X,upper_bound X.];

theorem :: RCOMP_3:16
  for X being real-bounded Subset of REAL st not upper_bound X in X
  holds X c= [.lower_bound X,upper_bound X.[;

theorem :: RCOMP_3:17
  for X being real-bounded interval Subset of REAL st lower_bound X in
  X & not upper_bound X in X holds X = [.lower_bound X,upper_bound X.[;

theorem :: RCOMP_3:18
  for X being real-bounded Subset of REAL st not lower_bound X in X &
  not upper_bound X in X holds X c= ].lower_bound X,upper_bound X.[;

theorem :: RCOMP_3:19
  for X being non empty real-bounded interval Subset of REAL st not
  lower_bound X in X & not upper_bound X in X holds X = ].lower_bound X,
  upper_bound X.[;

theorem :: RCOMP_3:20
  for X being Subset of REAL st X is bounded_above holds X c=
  left_closed_halfline(upper_bound X);

theorem :: RCOMP_3:21
  for X being interval Subset of REAL st X is not bounded_below &
  X is bounded_above & upper_bound X in X holds X = left_closed_halfline(
  upper_bound X);

theorem :: RCOMP_3:22
  for X being Subset of REAL st X is bounded_above & not
  upper_bound X in X holds X c= left_open_halfline(upper_bound X);

theorem :: RCOMP_3:23
  for X being non empty interval Subset of REAL st X is not
  bounded_below & X is bounded_above & not upper_bound X in X holds X =
  left_open_halfline(upper_bound X);

theorem :: RCOMP_3:24
  for X being Subset of REAL st X is bounded_below holds X c=
  right_closed_halfline(lower_bound X);

theorem :: RCOMP_3:25
  for X being interval Subset of REAL st X is bounded_below & X
  is not bounded_above & lower_bound X in X holds X = right_closed_halfline(
  lower_bound X);

theorem :: RCOMP_3:26
  for X being Subset of REAL st X is bounded_below & not
  lower_bound X in X holds X c= right_open_halfline(lower_bound X);

theorem :: RCOMP_3:27
  for X being non empty interval Subset of REAL st X is
  bounded_below & X is not bounded_above & not lower_bound X in X holds X =
  right_open_halfline(lower_bound X);

theorem :: RCOMP_3:28
  for X being interval Subset of REAL st X is not bounded_above &
  X is not bounded_below holds X = REAL;

theorem :: RCOMP_3:29
  for X being interval Subset of REAL holds X is empty or X =
  REAL or (ex a st X = left_closed_halfline(a)) or (ex a st X =
left_open_halfline(a)) or (ex a st X = right_closed_halfline(a)) or (ex a st X
= right_open_halfline(a)) or (ex a, b st a <= b & X = [.a,b.]) or (ex a, b st a
< b & X = [.a,b.[) or (ex a, b st a < b & X = ].a,b.]) or ex a, b st a < b & X
  = ].a,b.[;

theorem :: RCOMP_3:30
  for X being non empty interval Subset of REAL st not r in X
  holds r <= lower_bound X or upper_bound X <= r;

theorem :: RCOMP_3:31
  for X, Y being non empty real-bounded interval Subset of REAL st
lower_bound X <= lower_bound Y & upper_bound Y <= upper_bound X & (lower_bound
  X = lower_bound Y & lower_bound Y in Y implies lower_bound X in X) & (
upper_bound X = upper_bound Y & upper_bound Y in Y implies upper_bound X in X)
  holds Y c= X;

registration
  cluster open closed interval non empty non real-bounded for Subset of REAL;
end;

begin :: R^1

theorem :: RCOMP_3:32
  for X being Subset of R^1 st a <= b & X = [.a,b.] holds Fr X = { a,b};

theorem :: RCOMP_3:33
  for X being Subset of R^1 st a < b & X = ].a,b.[ holds Fr X = {a,b};

theorem :: RCOMP_3:34
  for X being Subset of R^1 st a < b & X = [.a,b.[ holds Fr X = {a ,b};

theorem :: RCOMP_3:35
  for X being Subset of R^1 st a < b & X = ].a,b.] holds Fr X = {a ,b};

theorem :: RCOMP_3:36
  for X being Subset of R^1 st X = [.a,b.] holds Int X = ].a,b.[;

theorem :: RCOMP_3:37
  for X being Subset of R^1 st X = ].a,b.[ holds Int X = ].a,b.[;

theorem :: RCOMP_3:38
  for X being Subset of R^1 st X = [.a,b.[ holds Int X = ].a,b.[;

theorem :: RCOMP_3:39
  for X being Subset of R^1 st X = ].a,b.] holds Int X = ].a,b.[;

registration let T be real-membered TopStruct, X be interval Subset of T;
 cluster T|X -> interval;
end;

registration
  let A be interval Subset of REAL;
  cluster R^1(A) -> interval;
end;

registration
 cluster connected -> interval for Subset of R^1;
 cluster interval -> connected for Subset of R^1;
end;

begin :: Closed Interval TSpace

registration
  let r;
  cluster Closed-Interval-TSpace(r,r) -> 1-element;
end;

theorem :: RCOMP_3:40
  r <= s implies for A being Subset of Closed-Interval-TSpace(r,s) holds
  A is real-bounded Subset of REAL;

theorem :: RCOMP_3:41
  r <= s implies for X being Subset of Closed-Interval-TSpace(r,s)
  st X = [.a,b.[ & r < a & b <= s holds Int X = ].a,b.[;

theorem :: RCOMP_3:42
  r <= s implies for X being Subset of Closed-Interval-TSpace(r,s)
  st X = ].a,b.] & r <= a & b < s holds Int X = ].a,b.[;

theorem :: RCOMP_3:43
  for X being Subset of Closed-Interval-TSpace(r,s), Y being
  Subset of REAL st X = Y holds X is connected iff Y is interval;

registration
  let T be TopSpace;
  cluster open closed connected for Subset of T;
end;

registration
  let T be non empty connected TopSpace;
  cluster non empty open closed connected for Subset of T;
end;

theorem :: RCOMP_3:44
  r <= s implies for X being open connected Subset of
Closed-Interval-TSpace(r,s) holds X is empty or X = [.r,s.] or (ex a being Real
 st r < a & a <= s & X = [.r,a.[) or (ex a being Real st r <= a &
a < s & X = ].a,s.]) or ex a, b being Real st r <= a & a < b & b <= s &
  X = ].a,b.[;

begin

theorem :: RCOMP_3:45
  for T being 1-sorted, F being finite Subset-Family of T for F1
being Subset-Family of T st F is Cover of T & F1 = F \ {X where X is Subset of
T: X in F & ex Y being Subset of T st Y in F & X c< Y} holds F1 is Cover of T;

theorem :: RCOMP_3:46
  for S being 1-element 1-sorted, s being Point of S, F
  being Subset-Family of S st F is Cover of S holds {s} in F;

definition
  let T be TopStruct, F be Subset-Family of T;
  attr F is connected means
:: RCOMP_3:def 1

  for X being Subset of T st X in F holds X is connected;
end;

registration
  let T be TopSpace;
  cluster non empty open closed connected for Subset-Family of T;
end;

reserve n, m for Nat,
  F for Subset-Family of Closed-Interval-TSpace (r,s);

theorem :: RCOMP_3:47
  for L being TopSpace, G, G1 being Subset-Family of L st G is
Cover of L & G is finite for ALL being set st G1 = G \ {X where X is Subset of
L: X in G & ex Y being Subset of L st Y in G & X c< Y} & ALL = {C where C is
  Subset-Family of L: C is Cover of L & C c= G1} holds ALL
  has_lower_Zorn_property_wrt RelIncl ALL;

theorem :: RCOMP_3:48
  for L being TopSpace, G, ALL being set st ALL = {C where C is
  Subset-Family of L: C is Cover of L & C c= G} for M being set st M
is_minimal_in RelIncl ALL & M in field RelIncl ALL for A1 being Subset of L st
  A1 in M holds not ex A2, A3 being Subset of L st A2 in M & A3 in M & A1 c= A2
  \/ A3 & A1 <> A2 & A1 <> A3;

registration let X be Subset-Family of REAL;
 cluster -> real-membered for Element of X;
end;

definition
  let r, s be Real;
  let F be Subset-Family of Closed-Interval-TSpace(r,s) such that
 F is Cover of Closed-Interval-TSpace(r,s) and
 F is open and
 F is connected and
 r <= s;
  mode IntervalCover of F -> FinSequence of bool REAL means
:: RCOMP_3:def 2

    rng it c= F
& union rng it = [.r,s.] & (for n being Nat st 1 <= n holds (n <=
len it implies it/.n is non empty) & (n+1 <= len it implies lower_bound(it/.n)
    <= lower_bound(it/.(n+1)) & upper_bound(it/.n) <= upper_bound(it/.(n+1)) &
    lower_bound(it/.(n+1)) < upper_bound(it/.n)) & (n+2 <= len it implies
upper_bound(it/.n) <= lower_bound(it/.(n+2)))) & ([.r,s.] in F implies it = <*
[.r,s.]*>) & (not [.r,s.] in F implies (ex p being Real st r < p & p <=
s & it.1 = [.r,p.[) & (ex p being Real st r <= p & p < s & it.len it =
].p,s.]) & for n being Nat st 1 < n & n < len it ex p, q being Real
 st r <= p & p < q & q <= s & it.n = ].p,q.[ );
end;

theorem :: RCOMP_3:49
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
  s & [.r,s.] in F implies <*[.r,s.]*> is IntervalCover of F;

reserve C for IntervalCover of F;

theorem :: RCOMP_3:50
  for F being Subset-Family of Closed-Interval-TSpace(r,r), C
being IntervalCover of F holds F is Cover of Closed-Interval-TSpace(r,r) & F is
  open connected implies C = <*[.r,r.]*>;

theorem :: RCOMP_3:51
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s implies 1 <= len C;

theorem :: RCOMP_3:52
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s & len C = 1 implies C = <*[.r,s.]*>;

theorem :: RCOMP_3:53
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s & n in dom C & m in dom C & n < m implies lower_bound(C/.n) <= lower_bound(C
  /.m);

theorem :: RCOMP_3:54
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s & n in dom C & m in dom C & n < m implies upper_bound(C/.n) <= upper_bound(C
  /.m);

theorem :: RCOMP_3:55
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & 1 <= n & n+1 <= len C implies ].lower_bound(C/.(n+1)),upper_bound(C
  /.n).[ is non empty;

theorem :: RCOMP_3:56
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
  s implies lower_bound(C/.1) = r;

theorem :: RCOMP_3:57
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s implies r in C/.1;

theorem :: RCOMP_3:58
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
  s implies upper_bound(C/.len C) = s;

theorem :: RCOMP_3:59
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s implies s in C/.len C;

definition
  let r, s be Real;
  let F be Subset-Family of Closed-Interval-TSpace(r,s), C be IntervalCover of
  F such that
 F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
  connected & r <= s;
  mode IntervalCoverPts of C -> FinSequence of REAL means
:: RCOMP_3:def 3

    len it = len
C + 1 & it.1 = r & it.len it = s & for n being Nat st 1 <= n & n+1 <
    len it holds it.(n+1) in ].lower_bound(C/.(n+1)),upper_bound(C/.n).[;
end;

reserve G for IntervalCoverPts of C;

theorem :: RCOMP_3:60
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s implies 2 <= len G;

theorem :: RCOMP_3:61
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s & len C = 1 implies G = <*r,s*>;

theorem :: RCOMP_3:62
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s & 1 <= n & n+1 < len G implies G.(n+1) < upper_bound(C/.n);

theorem :: RCOMP_3:63
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s & 1 < n & n <= len C implies lower_bound(C/.n) < G.n;

theorem :: RCOMP_3:64
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r <= s & 1 <= n & n < len C implies G.n <= lower_bound(C/.(n+1));

theorem :: RCOMP_3:65
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
  & r < s implies G is increasing;

theorem :: RCOMP_3:66
  F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
  s & 1 <= n & n < len G implies [.G.n,G.(n+1).] c= C.n;