:: Some Properties of the Intervals
:: by J\'ozef Bia\las
::
:: Received February 5, 1994
:: Copyright (c) 1994-2017 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;