:: Suprema and Infima of Intervals of Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received June 26, 2008
:: Copyright (c) 2008-2016 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, INT_1, SUBSET_1, XXREAL_0, FINSET_1, ARYTM_3, XBOOLE_0,
ARYTM_1, NAT_1, FUNCT_1, RELAT_1, TARSKI, ORDINAL1, MEMBERED, ORDINAL2,
FINSUB_1, SETWISEO, CARD_1, XREAL_0, RAT_1, XXREAL_1, XXREAL_2, MEASURE5,
REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
CARD_1, FINSUB_1, SETWISEO, NUMBERS, MEMBERED, XXREAL_0, XCMPLX_0,
XREAL_0, INT_1, NAT_1, RAT_1, XXREAL_1;
constructors XXREAL_0, MEMBERED, XREAL_0, INT_1, FINSET_1, RAT_1, XXREAL_1,
SETWISEO, XCMPLX_0, REAL_1, NAT_1, XTUPLE_0, CARD_1;
registrations XXREAL_0, MEMBERED, XXREAL_1, XBOOLE_0, FINSET_1, NUMBERS,
SETWISEO, FINSUB_1, XREAL_0, INT_1, NAT_1, CARD_1, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
scheme :: XXREAL_2:sch 1
FinInter{m, n() -> Integer, F(object)->object, P[object]}:
{F(i) where i is Element
of INT: m()<=i & i<=n() & P[i]} is finite;
reserve x,y,z,r,s for ExtReal;
definition
let X be ext-real-membered set;
mode UpperBound of X -> ExtReal means
:: XXREAL_2:def 1
x in X implies x <= it;
mode LowerBound of X -> ExtReal means
:: XXREAL_2:def 2
x in X implies it <= x;
end;
definition
let X be ext-real-membered set;
func sup X -> ExtReal means
:: XXREAL_2:def 3
it is UpperBound of X & for x being UpperBound of X holds it <= x;
func inf X -> ExtReal means
:: XXREAL_2:def 4
it is LowerBound of X & for x being LowerBound of X holds x <= it;
end;
definition
let X be ext-real-membered set;
attr X is left_end means
:: XXREAL_2:def 5
inf X in X;
attr X is right_end means
:: XXREAL_2:def 6
sup X in X;
end;
theorem :: XXREAL_2:1
y is UpperBound of {x} iff x <= y;
theorem :: XXREAL_2:2
y is LowerBound of {x} iff y <= x;
registration
cluster -> ext-real-membered for Element of Fin ExtREAL;
end;
reserve A,B for ext-real-membered set;
theorem :: XXREAL_2:3
x in A implies inf A <= x;
theorem :: XXREAL_2:4
x in A implies x <= sup A;
theorem :: XXREAL_2:5
B c= A implies for x being LowerBound of A holds x is LowerBound of B;
theorem :: XXREAL_2:6
B c= A implies for x being UpperBound of A holds x is UpperBound of B;
theorem :: XXREAL_2:7
for x being LowerBound of A, y being LowerBound of B holds min(x,
y) is LowerBound of A\/ B;
theorem :: XXREAL_2:8
for x being UpperBound of A, y being UpperBound of B holds max(x,
y) is UpperBound of A\/ B;
theorem :: XXREAL_2:9
inf(A \/ B) = min(inf A,inf B);
theorem :: XXREAL_2:10
sup(A \/ B) = max(sup A,sup B);
registration
cluster finite -> left_end right_end for non empty ext-real-membered set;
end;
registration
cluster -> left_end for non empty natural-membered set;
end;
registration
cluster right_end for non empty natural-membered set;
end;
notation
let X be left_end ext-real-membered set;
synonym min X for inf X;
end;
notation
let X be right_end ext-real-membered set;
synonym max X for sup X;
end;
definition
let X be left_end ext-real-membered set;
redefine func min X means
:: XXREAL_2:def 7
it in X & for x st x in X holds it <= x;
end;
definition
let X be right_end ext-real-membered set;
redefine func max X means
:: XXREAL_2:def 8
it in X & for x st x in X holds x <= it;
end;
theorem :: XXREAL_2:11
max{x} = x;
theorem :: XXREAL_2:12
max(x,y) = max{x,y};
theorem :: XXREAL_2:13
min{x} = x;
theorem :: XXREAL_2:14
min{x,y} = min(x,y);
definition
let X be ext-real-membered set;
attr X is bounded_below means
:: XXREAL_2:def 9
ex r being Real st r is LowerBound of X;
attr X is bounded_above means
:: XXREAL_2:def 10
ex r being Real st r is UpperBound of X;
end;
registration
cluster non empty finite natural-membered for set;
end;
definition
let X be ext-real-membered set;
attr X is real-bounded means
:: XXREAL_2:def 11
X is bounded_below bounded_above;
end;
registration
cluster real-bounded -> bounded_above bounded_below
for ext-real-membered set;
cluster bounded_above bounded_below -> real-bounded
for ext-real-membered set;
end;
registration
cluster finite -> real-bounded for real-membered set;
end;
registration
cluster real-bounded for non empty natural-membered set;
end;
theorem :: XXREAL_2:15
for X being non empty real-membered set st X is bounded_below
holds inf X in REAL;
theorem :: XXREAL_2:16
for X being non empty real-membered set st X is bounded_above
holds sup X in REAL;
registration
let X be bounded_above non empty real-membered set;
cluster sup X -> real;
end;
registration
let X be bounded_below non empty real-membered set;
cluster inf X -> real;
end;
registration
cluster bounded_above -> right_end for non empty integer-membered set;
end;
registration
cluster bounded_below -> left_end for non empty integer-membered set;
end;
registration
cluster -> bounded_below for natural-membered set;
end;
registration
let X be left_end real-membered set;
cluster min X -> real;
end;
registration
let X be left_end rational-membered set;
cluster min X -> rational;
end;
registration
let X be left_end integer-membered set;
cluster min X -> integer;
end;
registration
let X be left_end natural-membered set;
cluster min X -> natural;
end;
registration
let X be right_end real-membered set;
cluster max X -> real;
end;
registration
let X be right_end rational-membered set;
cluster max X -> rational;
end;
registration
let X be right_end integer-membered set;
cluster max X -> integer;
end;
registration
let X be right_end natural-membered set;
cluster max X -> natural;
end;
registration
cluster left_end -> bounded_below for real-membered set;
cluster right_end -> bounded_above for real-membered set;
end;
theorem :: XXREAL_2:17
x is LowerBound of [.x,y.];
theorem :: XXREAL_2:18
x is LowerBound of ].x,y.];
theorem :: XXREAL_2:19
x is LowerBound of [.x,y.[;
theorem :: XXREAL_2:20
x is LowerBound of ].x,y.[;
theorem :: XXREAL_2:21
y is UpperBound of [.x,y.];
theorem :: XXREAL_2:22
y is UpperBound of ].x,y.];
theorem :: XXREAL_2:23
y is UpperBound of [.x,y.[;
theorem :: XXREAL_2:24
y is UpperBound of ].x,y.[;
theorem :: XXREAL_2:25
x <= y implies inf [.x,y.] = x;
theorem :: XXREAL_2:26
x < y implies inf [.x,y.[ = x;
theorem :: XXREAL_2:27
x < y implies inf ].x,y.] = x;
theorem :: XXREAL_2:28
x < y implies inf ].x,y.[ = x;
theorem :: XXREAL_2:29
x <= y implies sup [.x,y.] = y;
theorem :: XXREAL_2:30
x < y implies sup ].x,y.] = y;
theorem :: XXREAL_2:31
x < y implies sup [.x,y.[ = y;
theorem :: XXREAL_2:32
x < y implies sup ].x,y.[ = y;
theorem :: XXREAL_2:33
x <= y implies [.x,y.] is left_end right_end;
theorem :: XXREAL_2:34
x < y implies [.x,y.[ is left_end;
theorem :: XXREAL_2:35
x < y implies ].x,y.] is right_end;
theorem :: XXREAL_2:36
x is LowerBound of {};
theorem :: XXREAL_2:37
x is UpperBound of {};
theorem :: XXREAL_2:38
inf {} = +infty;
theorem :: XXREAL_2:39
sup {} = -infty;
theorem :: XXREAL_2:40
for X being ext-real-membered set holds X is non empty iff inf X <= sup X;
registration
cluster real-bounded -> finite for integer-membered set;
end;
registration
cluster -> finite for bounded_above natural-membered set;
end;
theorem :: XXREAL_2:41
for X being ext-real-membered set holds +infty is UpperBound of X;
theorem :: XXREAL_2:42
for X being ext-real-membered set holds -infty is LowerBound of X;
theorem :: XXREAL_2:43
for X,Y being ext-real-membered set st X c= Y & Y is
bounded_above holds X is bounded_above;
theorem :: XXREAL_2:44
for X,Y being ext-real-membered set st X c= Y & Y is
bounded_below holds X is bounded_below;
theorem :: XXREAL_2:45
for X,Y being ext-real-membered set st X c= Y & Y is real-bounded holds
X is real-bounded;
theorem :: XXREAL_2:46
REAL is non bounded_below non bounded_above;
registration
cluster REAL -> non bounded_below non bounded_above;
end;
theorem :: XXREAL_2:47
{+infty} is bounded_below;
theorem :: XXREAL_2:48
{-infty} is bounded_above;
theorem :: XXREAL_2:49
for X being bounded_above non empty ext-real-membered set st X
<> {-infty} holds ex x being Element of REAL st x in X;
theorem :: XXREAL_2:50
for X being bounded_below non empty ext-real-membered set st X
<> {+infty} holds ex x being Element of REAL st x in X;
theorem :: XXREAL_2:51
for X being ext-real-membered set st -infty is UpperBound of X
holds X c= {-infty};
theorem :: XXREAL_2:52
for X being ext-real-membered set st +infty is LowerBound of X
holds X c= {+infty};
theorem :: XXREAL_2:53
for X being non empty ext-real-membered set st ex y being UpperBound
of X st y <> +infty holds X is bounded_above;
theorem :: XXREAL_2:54
for X being non empty ext-real-membered set st ex y being LowerBound
of X st y <> -infty holds X is bounded_below;
theorem :: XXREAL_2:55
for X being non empty ext-real-membered set, x being UpperBound of X
st x in X holds x = sup X;
theorem :: XXREAL_2:56
for X being non empty ext-real-membered set, x being LowerBound of X
st x in X holds x = inf X;
theorem :: XXREAL_2:57
for X being non empty ext-real-membered set st X is
bounded_above & X <> {-infty} holds sup X in REAL;
theorem :: XXREAL_2:58
for X being non empty ext-real-membered set st X is
bounded_below & X <> {+infty} holds inf X in REAL;
theorem :: XXREAL_2:59
for X,Y being ext-real-membered set st X c= Y holds sup X <= sup Y;
theorem :: XXREAL_2:60
for X,Y being ext-real-membered set st X c= Y holds inf Y <= inf X;
theorem :: XXREAL_2:61
for X being ext-real-membered set, x being ExtReal st (ex y
being ExtReal st y in X & x <= y) holds x <= sup X;
theorem :: XXREAL_2:62
for X being ext-real-membered set, x being ExtReal st (ex y
being ExtReal st y in X & y <= x) holds inf X <= x;
theorem :: XXREAL_2:63
for X,Y being ext-real-membered set st for x being ExtReal st
x in X ex y being ExtReal st y in Y & x <= y holds sup X <= sup Y;
theorem :: XXREAL_2:64
for X,Y being ext-real-membered set st for y being ExtReal st
y in Y ex x being ExtReal st x in X & x <= y holds inf X <= inf Y;
theorem :: XXREAL_2:65
for X,Y being ext-real-membered set, x being UpperBound of X, y
being UpperBound of Y holds min(x,y) is UpperBound of X /\ Y;
theorem :: XXREAL_2:66
for X,Y being ext-real-membered set, x being LowerBound of X, y
being LowerBound of Y holds max(x,y) is LowerBound of X /\ Y;
theorem :: XXREAL_2:67
for X,Y being ext-real-membered set holds sup(X /\ Y) <= min(sup X,sup Y);
theorem :: XXREAL_2:68
for X,Y being ext-real-membered set holds max(inf X,inf Y) <= inf(X /\ Y);
registration
cluster real-bounded -> real-membered for ext-real-membered set;
end;
theorem :: XXREAL_2:69
A c= [.inf A, sup A.];
theorem :: XXREAL_2:70
sup A = inf A implies A = {inf A};
theorem :: XXREAL_2:71
x <= y & x is UpperBound of A implies y is UpperBound of A;
theorem :: XXREAL_2:72
y <= x & x is LowerBound of A implies y is LowerBound of A;
theorem :: XXREAL_2:73
A is bounded_above iff sup A <> +infty;
theorem :: XXREAL_2:74
A is bounded_below iff inf A <> -infty;
begin :: Connectedness
definition
let A be ext-real-membered set;
attr A is interval means
:: XXREAL_2:def 12
for r,s being ExtReal st r in A & s in A holds [.r,s.] c= A;
end;
registration
cluster ExtREAL -> interval;
cluster empty -> interval for ext-real-membered set;
let r,s;
cluster [.r,s.] -> interval;
cluster ].r,s.] -> interval;
cluster [.r,s.[ -> interval;
cluster ].r,s.[ -> interval;
end;
registration
cluster REAL -> interval;
end;
registration
cluster interval for non empty ext-real-membered set;
end;
registration
let A,B be interval ext-real-membered set;
cluster A /\ B -> interval;
end;
reserve A,B for ext-real-membered set;
registration
let r,s;
cluster ].r,s.] -> non left_end;
cluster [.r,s.[ -> non right_end;
cluster ].r,s.[ -> non left_end non right_end;
end;
registration
cluster left_end right_end interval for ext-real-membered set;
cluster non left_end right_end interval for ext-real-membered set;
cluster left_end non right_end interval for ext-real-membered set;
cluster non left_end non right_end interval non empty for ext-real-membered
set;
end;
theorem :: XXREAL_2:75
for A being left_end right_end interval ext-real-membered set holds
A = [.min A, max A.];
theorem :: XXREAL_2:76
for A being non left_end right_end interval ext-real-membered set
holds A = ].inf A, max A.];
theorem :: XXREAL_2:77
for A being left_end non right_end interval ext-real-membered set
holds A = [.min A, sup A.[;
theorem :: XXREAL_2:78
for A being non left_end non right_end non empty interval
ext-real-membered set holds A =].inf A,sup A.[;
theorem :: XXREAL_2:79
for A being non left_end non right_end interval ext-real-membered
set ex r,s st r <= s & A =].r,s.[;
theorem :: XXREAL_2:80
A is interval implies for x,y,r st x in A & y in A & x <= r & r
<= y holds r in A;
theorem :: XXREAL_2:81
A is interval implies for x,r st x in A & x <= r & r < sup A holds r in A;
theorem :: XXREAL_2:82
A is interval implies for x,r st x in A & inf A < r & r <= x holds r in A;
theorem :: XXREAL_2:83
A is interval implies for r st inf A < r & r < sup A holds r in A;
theorem :: XXREAL_2:84
(for x,y,r st x in A & y in A & x < r & r < y holds r in A)
implies A is interval;
theorem :: XXREAL_2:85
(for x,r st x in A & x < r & r < sup A holds r in A) implies A is interval;
theorem :: XXREAL_2:86
(for y,r st y in A & inf A < r & r < y holds r in A) implies A is interval;
theorem :: XXREAL_2:87
(for r st inf A < r & r < sup A holds r in A) implies A is interval;
theorem :: XXREAL_2:88
(for x,y,r st x in A & y in A & x <= r & r <= y holds r in A)
implies A is interval;
theorem :: XXREAL_2:89
A is interval & B is interval & A meets B implies A \/ B is interval;
theorem :: XXREAL_2:90
A is interval & B is left_end interval & sup A = inf B implies A \/
B is interval;
theorem :: XXREAL_2:91
A is right_end interval & B is interval & sup A = inf B implies A \/
B is interval;
registration
cluster left_end -> non empty for ext-real-membered set;
cluster right_end -> non empty for ext-real-membered set;
end;
:: from HAHNBAN, 2011.04.26, A.T.
theorem :: XXREAL_2:92
for A being non empty Subset of ExtREAL st
for r being Element of ExtREAL st r in A
holds r <= -infty holds A = {-infty};
theorem :: XXREAL_2:93
for A being non empty Subset of ExtREAL st
for r being Element of ExtREAL st r in A
holds +infty <= r holds A = {+infty};
theorem :: XXREAL_2:94
for A being non empty Subset of ExtREAL, r being ExtReal
st r < sup A ex s being Element of ExtREAL st s in A & r < s;
theorem :: XXREAL_2:95
for A being non empty Subset of ExtREAL, r being Element of ExtREAL
st inf A < r
ex s being Element of ExtREAL st s in A & s < r;
theorem :: XXREAL_2:96
for A,B being non empty Subset of ExtREAL st for r,s being ExtReal
st r in A & s in B holds r <= s holds sup A <= inf B;