:: Some Properties of the Intervals
::  by J\'ozef Bia\las
::
:: Received February 5, 1994
:: Copyright (c) 1994-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, FUNCT_1, ZFMISC_1, RELAT_1, SUPINF_2, XXREAL_0, CARD_1,
      SUPINF_1, SUBSET_1, NAT_1, ARYTM_3, ORDINAL1, XXREAL_2, ORDINAL2,
      XBOOLE_0, REAL_1, ARYTM_1, MEASURE5, XXREAL_1, MEMBERED, MEMBER_1,
      TARSKI, XCMPLX_0, FREEALG, QUANTAL1, SETFAM_1, FINSET_1, COMPLEX1, SEQ_1,
      SEQ_2, VALUED_0, SEQ_4, PSCOMP_1, RCOMP_1, PRALG_1, PRE_TOPC, PARTFUN1,
      INT_1, ASYMPT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, FINSET_1,
      NUMBERS, MEMBERED, ABSVALUE, COMPLEX1, VALUED_0, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, MEMBER_1, FUNCT_3, XXREAL_0,
      XXREAL_1, XXREAL_2, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1,
      SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, SUPINF_1, SUPINF_2, MEASURE5,
      VALUED_1;
 constructors WELLORD2, DOMAIN_1, REAL_1, NAT_1, CARD_1, SUPINF_2, MEASURE5,
      SUPINF_1, RCOMP_1, RELSET_1, COMPLEX1, SEQ_2, SEQM_3, VALUED_0, VALUED_1,
      FUNCOP_1, SEQ_4, BINOP_2, LIMFUNC1, MEMBER_1, FUNCT_3, COMSEQ_2, SEQ_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XREAL_0,
      MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, VALUED_0, VALUED_1, NAT_1, INT_1,
      FINSET_1, MEMBER_1, RCOMP_1, SEQ_2, SEQ_4, FCONT_3, FUNCT_2, MEASURE5,
      RELSET_1, XCMPLX_0, SEQ_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Some theorems about R_eal numbers

theorem :: MEASURE6:1
  ex F being sequence of [:NAT,NAT:]
  st F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:];

theorem :: MEASURE6:2
  for F being sequence of ExtREAL st F is nonnegative holds 0. <= SUM(F);

theorem :: MEASURE6:3
  for F being sequence of ExtREAL, x being R_eal st
  (ex n being Element of NAT st x <= F.n) & F is nonnegative holds x <= SUM(F);

definition
::$CD
end;

theorem :: MEASURE6:4
  for eps being ExtReal st 0. < eps ex F being sequence of ExtREAL st
  (for n being Nat holds 0. < F.n) & SUM(F) < eps;

theorem :: MEASURE6:5
  for eps being ExtReal, X being non empty Subset of ExtREAL st
  0. < eps & inf X is Real holds
  ex x being ExtReal st x in X & x < inf X + eps;

theorem :: MEASURE6:6
  for eps being ExtReal, X being non empty Subset of ExtREAL st
  0. < eps & sup X is Real holds ex x being ExtReal st
  x in X & sup X - eps < x;

theorem :: MEASURE6:7
  for F being sequence of  ExtREAL st F is nonnegative & SUM(F) < +infty
    holds for n being Element of NAT holds F.n in REAL;

:: PROPERTIES OF THE INTERVALS

registration
  cluster non empty interval for Subset of REAL;
end;

theorem :: MEASURE6:8
  for A being non empty Interval, a being ExtReal st
 ex b being ExtReal st a
  <= b & A = ].a,b.[ holds a = inf A;

theorem :: MEASURE6:9
  for A being non empty Interval, a being ExtReal st
   ex b being ExtReal st a
  <= b & A = ].a,b.] holds a = inf A;

theorem :: MEASURE6:10
  for A being non empty Interval, a being ExtReal
    st ex b being ExtReal st a <= b & A = [.a,b.]
 holds a = inf A;

theorem :: MEASURE6:11
  for A being non empty Interval, a being ExtReal st
   ex b being ExtReal st a <= b & A = [.a,b.[ holds a = inf A;

theorem :: MEASURE6:12
  for A being non empty Interval, b being ExtReal
   st ex a being ExtReal st a
  <= b & A = ].a,b.[ holds b = sup A;

theorem :: MEASURE6:13
  for A being non empty Interval, b being ExtReal st ex a being
  ExtReal st a <= b & A = ].a,b.] holds b = sup A;

theorem :: MEASURE6:14
  for A being non empty Interval, b being ExtReal st
  ex a being ExtReal st a <= b & A = [.a,b.] holds b = sup A;

theorem :: MEASURE6:15
  for A being non empty Interval, b being ExtReal st
    ex a being ExtReal st a <= b & A = [.a,b.[ holds b = sup A;

theorem :: MEASURE6:16
  for A being non empty Interval st A is open_interval
     holds A = ].inf A,sup A.[;

theorem :: MEASURE6:17
  for A being non empty Interval st A is closed_interval holds
    A = [.inf A,sup A.];

theorem :: MEASURE6:18
  for A being non empty Interval st A is right_open_interval holds
  A = [.inf A,sup A.[;

theorem :: MEASURE6:19
  for A being non empty Interval st A is left_open_interval holds
   A = ].inf A,sup A.];

theorem :: MEASURE6:20
  for A,B being non empty Interval, a,b being Real st
    a in A & b in B & sup A <= inf B holds a <= b;

theorem :: MEASURE6:21
  for A,B be real-membered set holds for y being Real holds y in B ++ A iff
    ex x,z being Real st x in B & z in A & y = x + z;

theorem :: MEASURE6:22
  for A,B being non empty Interval holds sup A = inf B &
  (sup A in A or inf B in B) implies A \/ B is Interval;

definition
  let A be real-membered set;
  let x be Real;
  redefine func x ++ A -> Subset of REAL;
end;

theorem :: MEASURE6:23
  for A being Subset of REAL, x being Real holds -x ++ (x ++ A) = A;

theorem :: MEASURE6:24
  for x being Real, A being Subset of REAL st A = REAL holds x ++ A = A;

theorem :: MEASURE6:25
  for x being Real holds x ++ {} = {};

theorem :: MEASURE6:26
  for A being Interval, x being Real holds
    A is open_interval iff x ++ A is open_interval;

theorem :: MEASURE6:27
  for A being Interval, x being Real holds
    A is closed_interval iff x ++ A is closed_interval;

theorem :: MEASURE6:28
  for A being Interval, x being Real holds
    A is right_open_interval iff x ++ A is right_open_interval;

theorem :: MEASURE6:29
  for A being Interval, x being Real holds
    A is left_open_interval iff x ++ A is left_open_interval;

theorem :: MEASURE6:30
  for A being Interval, x being Real holds x ++ A is Interval;

theorem :: MEASURE6:31
  for A being real-membered set, x being Real,
      y being R_eal st x = y holds sup(x ++ A) = y + sup A;

theorem :: MEASURE6:32
  for A being real-membered set, x being Real,
      y being R_eal st x = y holds inf(x ++ A) = y + inf A;

theorem :: MEASURE6:33
  for A being Interval, x being Real holds
    diameter(A) = diameter(x ++ A);

begin :: from PSCOMP_1, 2010.02.26, A.T.

notation
  let X be set;
  synonym X is without_zero for X is with_non-empty_elements;
  antonym X is with_zero for X is with_non-empty_elements;
end;

definition
  let X be set;
  redefine attr X is without_zero means
:: MEASURE6:def 2

  not 0 in X;
end;

registration
  cluster REAL -> with_zero;
  cluster NAT -> with_zero;
end;

registration
  cluster non empty without_zero for set;
  cluster non empty with_zero for set;
end;

registration
  cluster non empty without_zero for Subset of REAL;
  cluster non empty with_zero for Subset of REAL;
end;

theorem :: MEASURE6:34
  for F being set st
    F is non empty with_non-empty_elements c=-linear holds F is centered;

registration
  let F be set;
  cluster non empty with_non-empty_elements c=-linear -> centered
    for Subset-Family of F;
end;

registration ::: FUNCT_2
  let X, Y be non empty set, f be Function of X, Y;
  cluster f.:X -> non empty;
end;

definition ::: FUNCT_3
  let X, Y be set, f be Function of X, Y;
  func "f -> Function of bool Y, bool X means
:: MEASURE6:def 3
  for y being Subset of Y holds it.y = f"y;
end;

theorem :: MEASURE6:35
  for X, Y, x being set, S being Subset-Family of Y, f being
  Function of X, Y st x in meet (("f).:S) holds f.x in meet S;

reserve r, s, t for Real;

theorem :: MEASURE6:36  ::: SQUARE_1 or ABSVALUE
  |.r.| + |.s.| = 0 implies r = 0;

theorem :: MEASURE6:37  ::: SQUARE_1 or ABSVALUE
  r < s & s < t implies |.s.| < |.r.| + |.t.|;

reserve seq for Real_Sequence,
  X, Y for Subset of REAL;

theorem :: MEASURE6:38  ::: SEQ_2
  seq is convergent & seq is non-zero & lim seq = 0 implies seq" is non bounded
;

theorem :: MEASURE6:39  ::: SEQ_2
  rng seq is real-bounded iff seq is bounded;

notation
  let X be real-membered set;
  synonym X is with_max for X is right_end;
  synonym X is with_min for X is left_end;
end;

definition
  let X be real-membered set;
  redefine attr X is with_max means
:: MEASURE6:def 4
  X is bounded_above & upper_bound X in X;
  redefine attr X is with_min means
:: MEASURE6:def 5
  X is bounded_below & lower_bound X in X;
end;

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

definition
  let R be Subset-Family of REAL;
  attr R is open means
:: MEASURE6:def 6
  for X being Subset of REAL st X in R holds X is open;
  attr R is closed means
:: MEASURE6:def 7

  for X being Subset of REAL st X in R holds X is closed;
end;

reserve r3, r1, q3, p3 for Real;

definition let X be Subset of REAL;
  redefine func --X -> Subset of REAL;
end;

theorem :: MEASURE6:40
  r in X iff -r in --X;

theorem :: MEASURE6:41
  X is bounded_above iff --X is bounded_below;

theorem :: MEASURE6:42
  X is bounded_below iff --X is bounded_above;

theorem :: MEASURE6:43
  for X being non empty Subset of REAL st X is bounded_below holds
  lower_bound X = - upper_bound --X;

theorem :: MEASURE6:44
  for X being non empty Subset of REAL st X is bounded_above holds
  upper_bound X = - lower_bound --X;

theorem :: MEASURE6:45
  X is closed iff --X is closed;

theorem :: MEASURE6:46
  r in X iff q3+r in q3++X;

theorem :: MEASURE6:47
  X = 0++X;

theorem :: MEASURE6:48
  q3++(p3++X) = (q3+p3)++X;

theorem :: MEASURE6:49
  X is bounded_above iff q3++X is bounded_above;

theorem :: MEASURE6:50
  X is bounded_below iff q3++X is bounded_below;

theorem :: MEASURE6:51
  for X being non empty Subset of REAL st X is bounded_below
   holds lower_bound (q3++X) = q3+lower_bound X;

theorem :: MEASURE6:52
  for X being non empty Subset of REAL st X is bounded_above
  holds upper_bound (q3++X) = q3+upper_bound X;

theorem :: MEASURE6:53
  X is closed iff q3++X is closed;

definition
  let X be Subset of REAL;
  func Inv X -> Subset of REAL equals
:: MEASURE6:def 8
  { 1/r3 : r3 in X };
  involutiveness;
end;

theorem :: MEASURE6:54
  for X being Subset of REAL holds r in X iff 1/r in Inv X;

registration
  let X be non empty Subset of REAL;
  cluster Inv X -> non empty;
end;

registration
  let X be without_zero Subset of REAL;
  cluster Inv X -> without_zero;
end;

theorem :: MEASURE6:55
  for X being without_zero Subset of REAL st X is closed real-bounded
  holds Inv X is closed;

theorem :: MEASURE6:56
  for Z being Subset-Family of REAL st Z is closed holds meet Z is closed;

definition
  let X be real-membered set;
  func Cl X -> Subset of REAL equals
:: MEASURE6:def 9
  meet { A where A is Subset of REAL : X c= A & A is closed };
  projectivity;
end;

registration
  let X be real-membered set;
  cluster Cl X -> closed;
end;

theorem :: MEASURE6:57
  for Y being closed Subset of REAL st X c= Y holds Cl X c= Y;

theorem :: MEASURE6:58
  for X being real-membered set holds X c= Cl X;

theorem :: MEASURE6:59
  X is closed iff X = Cl X;

theorem :: MEASURE6:60
  Cl ({}REAL) = {};

theorem :: MEASURE6:61
  Cl ([#]REAL) = REAL;

theorem :: MEASURE6:62
  for X, Y being real-membered set holds
  X c= Y implies Cl X c= Cl Y;

theorem :: MEASURE6:63
  r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
  O /\ X is non empty;

theorem :: MEASURE6:64
  r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3;

begin :: Functions into Reals

definition
  let X be set, f be Function of X, REAL;
  redefine attr f is bounded_below means
:: MEASURE6:def 10
  f.:X is bounded_below;
  redefine attr f is bounded_above means
:: MEASURE6:def 11
  f.:X is bounded_above;
end;

definition
  let X be set, f be Function of X, REAL;
  attr f is with_max means
:: MEASURE6:def 12
  f.:X is with_max;
  attr f is with_min means
:: MEASURE6:def 13
  f.:X is with_min;
end;

theorem :: MEASURE6:65
  for X, A being set, f being Function of X, REAL holds (-f).:A = --(f.:A);

theorem :: MEASURE6:66
  for X being non empty set, f being Function of X, REAL holds
  f is with_min iff -f is with_max;

theorem :: MEASURE6:67
  for X being non empty set, f being Function of X, REAL holds
  f is with_max iff -f is with_min;

theorem :: MEASURE6:68
  for X being set, A being Subset of REAL, f being Function of X, REAL
    holds (-f)"A = f"(--A);

theorem :: MEASURE6:69
  for X, A being set, f being Function of X, REAL, s being Real holds
    (s+f).:A = s++(f.:A);

theorem :: MEASURE6:70
  for X being set, A being Subset of REAL,
      f being Function of X,REAL, q3 holds (q3+f)"A = f"(-q3++A);

notation
  let f be real-valued Function;
  synonym Inv f for f";
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  redefine func Inv f -> PartFunc of C,REAL;
end;

theorem :: MEASURE6:71
  for X being set, A being without_zero Subset of REAL,
      f being Function of X, REAL holds (Inv f)"A = f"(Inv A);

theorem :: MEASURE6:72
  for A being Subset of REAL, x being Real st x in --A holds
    ex a being Real st a in A & x = -a;