:: Suprema and Infima of Intervals of Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received June 26, 2008
:: Copyright (c) 2008-2026 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;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, MEMBERED;
equalities ORDINAL1;
theorems XXREAL_0, MEMBERED, TARSKI, XBOOLE_0, XXREAL_1, XBOOLE_1, FINSUB_1,
XREAL_0, XREAL_1, INT_1, NAT_1, FINSET_1, ZFMISC_1, FUNCT_1, SETFAM_1;
schemes XXREAL_1, NAT_1, SETWISEO, CLASSES1;
begin
scheme
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;
set F = {F(i) where i is Element of INT: m()<=i & i<=n() & P[i]};
per cases;
suppose
A1: n() < m();
now
assume F <> {};
then consider x being object such that
A2: x in F by XBOOLE_0:def 1;
ex i being Element of INT st x = F(i) & m()<=i & i<=n() & P[i] by A2;
hence contradiction by A1,XXREAL_0:2;
end;
then reconsider F as empty set;
F is finite;
hence thesis;
end;
suppose
m() <= n();
then reconsider k = n()-m() as Element of NAT by INT_1:5;
set F = {F(i) where i is Element of INT: m()<=i & i<=n() & P[i]};
defpred Q[object,object] means
ex i being Integer st $1 = i & $2 = F(i+m());
A3: for e being object st e in k+1 ex u being object st Q[e,u]
proof
let e be object;
assume e in k+1;
then e in Segm(k+1);
then reconsider i = e as Nat;
take F(i+m()),i;
thus thesis;
end;
consider f being Function such that
A4: dom f = k+1 and
A5: for i being object st i in k+1 holds Q[i,f.i] from CLASSES1:sch 1(A3);
A6: F c= rng f
proof
let x be object;
assume x in F;
then consider j being Element of INT such that
A7: x=F(j) and
A8: m()<=j and
A9: j<=n() and
P[j];
reconsider l = j-m() as Element of NAT by A8,INT_1:5;
l <= k by A9,XREAL_1:9;
then l < k+1 by NAT_1:13;
then
A10: l in Segm(k+1) by NAT_1:44;
then Q[j-m(),f.(j-m())] by A5;
then f.(j-m()) = F(j+m()-m()) .= F(j);
hence thesis by A4,A7,A10,FUNCT_1:def 3;
end;
rng f is finite by A4,FINSET_1:8;
hence thesis by A6;
end;
end;
reserve x,y,z,r,s for ExtReal;
definition
let X be ext-real-membered set;
mode UpperBound of X -> ExtReal means
:Def1:
x in X implies x <= it;
existence
proof
take +infty;
thus thesis by XXREAL_0:4;
end;
mode LowerBound of X -> ExtReal means
:Def2:
x in X implies it <= x;
existence
proof
take -infty;
thus thesis by XXREAL_0:5;
end;
end;
definition
let X be ext-real-membered set;
func sup X -> ExtReal means
:Def3:
it is UpperBound of X & for x being UpperBound of X holds it <= x;
existence
proof
defpred Q[object] means $1 is UpperBound of X;
defpred P[object] means $1 in X;
A1: for r,s st P[r] & Q[s] holds r <= s by Def1;
consider s such that
A2: for r st P[r] holds r <= s and
A3: for r st Q[r] holds s <= r from XXREAL_1:sch 1(A1);
take s;
thus s is UpperBound of X by A2,Def1;
thus thesis by A3;
end;
uniqueness
proof
let y,z such that
A4: y is UpperBound of X and
A5: for x being UpperBound of X holds y <= x and
A6: z is UpperBound of X and
A7: for x being UpperBound of X holds z <= x;
A8: y <= z by A5,A6;
z <= y by A4,A7;
hence thesis by A8,XXREAL_0:1;
end;
func inf X -> ExtReal means
:Def4:
it is LowerBound of X & for x being LowerBound of X holds x <= it;
existence
proof
defpred Q[object] means $1 in X;
defpred P[object] means $1 is LowerBound of X;
A9: for r,s st P[r] & Q[s] holds r <= s by Def2;
consider s such that
A10: for r st P[r] holds r <= s and
A11: for r st Q[r] holds s <= r from XXREAL_1:sch 1(A9);
take s;
thus s is LowerBound of X by A11,Def2;
thus thesis by A10;
end;
uniqueness
proof
let y,z such that
A12: y is LowerBound of X and
A13: for x being LowerBound of X holds x <= y and
A14: z is LowerBound of X and
A15: for x being LowerBound of X holds x <= z;
A16: z <= y by A13,A14;
y <= z by A12,A15;
hence thesis by A16,XXREAL_0:1;
end;
end;
definition
let X be ext-real-membered set;
attr X is left_end means
:Def5:
inf X in X;
attr X is right_end means
:Def6:
sup X in X;
end;
theorem Th1:
y is UpperBound of {x} iff x <= y
proof
x in {x} by TARSKI:def 1;
hence y is UpperBound of {x} implies x <= y by Def1;
assume
A1: x <= y;
let z;
assume z in {x};
hence thesis by A1,TARSKI:def 1;
end;
theorem Th2:
y is LowerBound of {x} iff y <= x
proof
x in {x} by TARSKI:def 1;
hence y is LowerBound of {x} implies y <= x by Def2;
assume
A1: y <= x;
let z;
assume z in {x};
hence thesis by A1,TARSKI:def 1;
end;
Lm1: sup {x} = x
proof
A1: for z being UpperBound of {x} holds x <= z
proof
let z be UpperBound of {x};
x in {x} by TARSKI:def 1;
hence thesis by Def1;
end;
x is UpperBound of {x} by Th1;
hence thesis by A1,Def3;
end;
Lm2: inf {x} = x
proof
A1: for z being LowerBound of {x} holds z <= x
proof
let z be LowerBound of {x};
x in {x} by TARSKI:def 1;
hence thesis by Def2;
end;
x is LowerBound of {x} by Th2;
hence thesis by A1,Def4;
end;
registration
cluster -> ext-real-membered for Element of Fin ExtREAL;
coherence
proof
let X be Element of Fin ExtREAL;
X c= ExtREAL by FINSUB_1:def 5;
hence thesis;
end;
end;
reserve A,B for ext-real-membered set;
theorem Th3:
x in A implies inf A <= x
proof
inf A is LowerBound of A by Def4;
hence thesis by Def2;
end;
theorem Th4:
x in A implies x <= sup A
proof
sup A is UpperBound of A by Def3;
hence thesis by Def1;
end;
theorem Th5:
B c= A implies for x being LowerBound of A holds x is LowerBound of B
proof
assume
A1: B c= A;
let x be LowerBound of A;
let y;
assume y in B;
hence thesis by A1,Def2;
end;
theorem Th6:
B c= A implies for x being UpperBound of A holds x is UpperBound of B
proof
assume
A1: B c= A;
let x be UpperBound of A;
let y;
assume y in B;
hence thesis by A1,Def1;
end;
theorem Th7:
for x being LowerBound of A, y being LowerBound of B holds min(x,
y) is LowerBound of A\/ B
proof
let x be LowerBound of A, y be LowerBound of B;
set m = min(x,y);
let z;
assume
A1: z in A \/ B;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: z in A;
A3: m <= x by XXREAL_0:17;
x <= z by A2,Def2;
hence thesis by A3,XXREAL_0:2;
end;
suppose
A4: z in B;
A5: m <= y by XXREAL_0:17;
y <= z by A4,Def2;
hence thesis by A5,XXREAL_0:2;
end;
end;
theorem Th8:
for x being UpperBound of A, y being UpperBound of B holds max(x,
y) is UpperBound of A\/ B
proof
let x be UpperBound of A, y be UpperBound of B;
set m = max(x,y);
let z;
assume
A1: z in A \/ B;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: z in A;
A3: x <= m by XXREAL_0:25;
z <= x by A2,Def1;
hence thesis by A3,XXREAL_0:2;
end;
suppose
A4: z in B;
A5: y <= m by XXREAL_0:25;
z <= y by A4,Def1;
hence thesis by A5,XXREAL_0:2;
end;
end;
theorem Th9:
inf(A \/ B) = min(inf A,inf B)
proof
set m = min(inf A,inf B);
A1: inf B is LowerBound of B by Def4;
A2: for x being LowerBound of A \/ B holds x <= m
proof
let x be LowerBound of A \/ B;
x is LowerBound of B by Th5,XBOOLE_1:7;
then
A3: x <= inf B by Def4;
x is LowerBound of A by Th5,XBOOLE_1:7;
then x <= inf A by Def4;
hence thesis by A3,XXREAL_0:20;
end;
inf A is LowerBound of A by Def4;
then m is LowerBound of A \/ B by A1,Th7;
hence thesis by A2,Def4;
end;
theorem Th10:
sup(A \/ B) = max(sup A,sup B)
proof
set m = max(sup A,sup B);
A1: sup B is UpperBound of B by Def3;
A2: for x being UpperBound of A \/ B holds m <= x
proof
let x be UpperBound of A \/ B;
x is UpperBound of B by Th6,XBOOLE_1:7;
then
A3: sup B <= x by Def3;
x is UpperBound of A by Th6,XBOOLE_1:7;
then sup A <= x by Def3;
hence thesis by A3,XXREAL_0:28;
end;
sup A is UpperBound of A by Def3;
then m is UpperBound of A \/ B by A1,Th8;
hence thesis by A2,Def3;
end;
registration
cluster finite -> left_end right_end for non empty ext-real-membered set;
coherence
proof
let X be non empty ext-real-membered set;
defpred P[non empty ext-real-membered set] means $1 is left_end right_end;
assume
A1: X is finite;
X c= ExtREAL by MEMBERED:2;
then
A2: X is non empty Element of Fin ExtREAL by A1,FINSUB_1:def 5;
A3: for B1,B2 being non empty Element of Fin ExtREAL holds P[B1] & P[B2]
implies P[B1 \/ B2]
proof
let B1,B2 be non empty Element of Fin ExtREAL;
assume
A4: P[B1];
inf(B1 \/ B2) = min(inf B1,inf B2) by Th9;
then
A5: inf(B1 \/ B2) = inf B1 or inf(B1 \/ B2) = inf B2 by XXREAL_0:15;
assume
A6: P[B2];
then
A7: inf B2 in B2 by Def5;
inf B1 in B1 by A4,Def5;
hence inf(B1 \/ B2) in B1 \/ B2 by A7,A5,XBOOLE_0:def 3;
sup(B1 \/ B2) = max(sup B1,sup B2) by Th10;
then
A8: sup(B1 \/ B2) = sup B1 or sup(B1 \/ B2) = sup B2 by XXREAL_0:16;
A9: sup B2 in B2 by A6,Def6;
sup B1 in B1 by A4,Def6;
hence sup(B1 \/ B2) in B1 \/ B2 by A9,A8,XBOOLE_0:def 3;
end;
A10: for x being Element of ExtREAL holds P[{.x.}]
proof
let x being Element of ExtREAL;
sup {x} = x by Lm1;
then
A11: sup {x} in {x} by TARSKI:def 1;
inf {x} = x by Lm2;
then inf {x} in {x} by TARSKI:def 1;
hence thesis by A11,Def5,Def6;
end;
for B being non empty Element of Fin ExtREAL holds P[B] from SETWISEO
:sch 3(A10,A3);
hence thesis by A2;
end;
end;
registration
cluster -> left_end for non empty natural-membered set;
coherence
proof
let X be non empty natural-membered set;
defpred P[set] means $1 in X;
A1: ex k being Nat st P[k] by MEMBERED:12;
consider k being Nat such that
A2: P[k] and
A3: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A1);
A4: k is LowerBound of X
proof
let y;
assume y in X;
hence thesis by A3;
end;
for x being LowerBound of X holds x <= k by A2,Def2;
hence inf X in X by A2,A4,Def4;
end;
end;
registration
cluster right_end for non empty natural-membered set;
existence
proof
take {0};
thus thesis;
end;
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 :: redefines min (XXREAL_2, synonym) → inf (XXREAL_2, definition)
:Def7:
it in X & for x st x in X holds it <= x;
compatibility
proof
let y;
thus y = min X implies y in X & for x st x in X holds y <= x by Def5,Th3;
assume that
A1: y in X and
A2: for x st x in X holds y <= x;
A3: for x being LowerBound of X holds x <= y by A1,Def2;
y is LowerBound of X by A2,Def2;
hence thesis by A3,Def4;
end;
end;
definition
let X be right_end ext-real-membered set;
redefine func max X means :: redefines max (XXREAL_2, synonym) → sup (XXREAL_2, definition)
:Def8:
it in X & for x st x in X holds x <= it;
compatibility
proof
let y;
thus y = max X implies y in X & for x st x in X holds x <= y by Def6,Th4;
assume that
A1: y in X and
A2: for x st x in X holds x <= y;
A3: for x being UpperBound of X holds y <= x by A1,Def1;
y is UpperBound of X by A2,Def1;
hence thesis by A3,Def3;
end;
end;
theorem
max{x} = x by Lm1;
Lm3: x <= y implies y is UpperBound of {x,y}
proof
assume
A1: x <= y;
let z;
assume z in {x,y};
hence thesis by A1,TARSKI:def 2;
end;
Lm4: for z being UpperBound of {x,y} holds y <= z
proof
let z be UpperBound of {x,y};
y in {x,y} by TARSKI:def 2;
hence thesis by Def1;
end;
theorem
max(x,y) = max{x,y}
proof
now
per cases;
case
A1: x <= y;
A2: for z being UpperBound of {x,y} holds y <= z by Lm4;
y is UpperBound of {x,y} by A1,Lm3;
hence max{x,y} = y by A2,Def3;
end;
case
A3: y < x;
A4: for z being UpperBound of {x,y} holds x <= z by Lm4;
x is UpperBound of {x,y} by A3,Lm3;
hence max{x,y} = x by A4,Def3;
end;
end;
hence thesis by XXREAL_0:def 10;
end;
theorem
min{x} = x by Lm2;
Lm5: y <= x implies y is LowerBound of {x,y}
proof
assume
A1: y <= x;
let z;
assume z in {x,y};
hence thesis by A1,TARSKI:def 2;
end;
Lm6: for z being LowerBound of {x,y} holds z <= y
proof
let z be LowerBound of {x,y};
y in {x,y} by TARSKI:def 2;
hence thesis by Def2;
end;
theorem
min{x,y} = min(x,y)
proof
now
per cases;
case
A1: y <= x;
A2: for z being LowerBound of {x,y} holds z <= y by Lm6;
y is LowerBound of {x,y} by A1,Lm5;
hence min{x,y} = y by A2,Def4;
end;
case
A3: x < y;
A4: for z being LowerBound of {x,y} holds z <= x by Lm6;
x is LowerBound of {x,y} by A3,Lm5;
hence min{x,y} = x by A4,Def4;
end;
end;
hence thesis by XXREAL_0:def 9;
end;
definition
let X be ext-real-membered set;
attr X is bounded_below means
:Def9:
ex r being Real st r is LowerBound of X;
attr X is bounded_above means
:Def10:
ex r being Real st r is UpperBound of X;
end;
registration
cluster non empty finite natural-membered for set;
existence
proof
take {0};
thus thesis;
end;
end;
definition
let X be ext-real-membered set;
attr X is real-bounded means
X is bounded_below bounded_above;
end;
registration
cluster real-bounded -> bounded_above bounded_below
for ext-real-membered set;
coherence;
cluster bounded_above bounded_below -> real-bounded
for ext-real-membered set;
coherence;
end;
registration
cluster finite -> real-bounded for real-membered set;
coherence
proof
let X be real-membered set;
assume
A1: X is finite;
per cases;
suppose
A2: X is empty;
thus X is bounded_below
proof
take 0;
let x;
thus thesis by A2;
end;
take 0;
let x;
thus thesis by A2;
end;
suppose
X is non empty;
then reconsider Y=X as non empty finite real-membered set by A1;
inf Y in X by Def5;
then reconsider m = inf X as Real;
thus X is bounded_below
proof
take m;
let x;
assume x in X;
hence thesis by Th3;
end;
sup Y in X by Def6;
then reconsider m = sup X as Real;
take m;
let x;
assume x in X;
hence thesis by Th4;
end;
end;
end;
registration
cluster real-bounded for non empty natural-membered set;
existence
proof
take {0};
thus thesis;
end;
end;
theorem Th15:
for X being non empty real-membered set st X is bounded_below
holds inf X in REAL
proof
let X be non empty real-membered set;
given r being Real such that
A1: r is LowerBound of X;
consider s being Real such that
A2: s in X by MEMBERED:9;
A3: inf X <= s by A2,Th3;
A4: r in REAL by XREAL_0:def 1;
A5: s in REAL by XREAL_0:def 1;
r <= inf X by A1,Def4;
hence thesis by A4,A5,A3,XXREAL_0:45;
end;
theorem Th16:
for X being non empty real-membered set st X is bounded_above
holds sup X in REAL
proof
let X be non empty real-membered set;
given r being Real such that
A1: r is UpperBound of X;
consider s being Real such that
A2: s in X by MEMBERED:9;
A3: s <= sup X by A2,Th4;
A4: r in REAL by XREAL_0:def 1;
A5: s in REAL by XREAL_0:def 1;
sup X <= r by A1,Def3;
hence thesis by A4,A5,A3,XXREAL_0:45;
end;
registration
let X be bounded_above non empty real-membered set;
cluster sup X -> real;
coherence
proof
sup X in REAL by Th16;
hence thesis;
end;
end;
registration
let X be bounded_below non empty real-membered set;
cluster inf X -> real;
coherence
proof
inf X in REAL by Th15;
hence thesis;
end;
end;
registration
cluster bounded_above -> right_end for non empty integer-membered set;
coherence
proof
let X be non empty integer-membered set;
assume X is bounded_above;
then reconsider Y=X as bounded_above non empty integer-membered set;
set s = sup Y;
A1: [\ s /] <= s by INT_1:def 6;
[\ s /] is UpperBound of X
proof
let x;
assume x in X;
hence thesis by Th4,INT_1:54;
end;
then s <= [\ s /] by Def3;
then reconsider s as Integer by A1,XXREAL_0:1;
assume
A2: not sup X in X;
s - 1 is UpperBound of X
proof
let x;
assume
A3: x in X;
then reconsider i=x as Integer;
i <= s by A3,Th4;
then i < s by A2,A3,XXREAL_0:1;
hence thesis by INT_1:52;
end;
then s - 1 >= s by Def3;
hence contradiction by XREAL_1:146;
end;
end;
registration
cluster bounded_below -> left_end for non empty integer-membered set;
coherence
proof
let X be non empty integer-membered set;
assume X is bounded_below;
then reconsider Y=X as bounded_below non empty integer-membered set;
set s = inf Y;
A1: [/ s \] >= s by INT_1:def 7;
[/ s \] is LowerBound of X
proof
let x;
assume x in X;
hence thesis by Th3,INT_1:65;
end;
then [/ s \] <= s by Def4;
then reconsider s as Integer by A1,XXREAL_0:1;
assume
A2: not inf X in X;
s + 1 is LowerBound of X
proof
let x;
assume
A3: x in X;
then reconsider i=x as Integer;
i >= s by A3,Th3;
then s < i by A2,A3,XXREAL_0:1;
hence thesis by INT_1:7;
end;
then s + 1 <= s by Def4;
hence contradiction by XREAL_1:145;
end;
end;
registration
cluster -> bounded_below for natural-membered set;
coherence
proof
let X be natural-membered set;
take 0;
let x;
assume x in X;
hence thesis;
end;
end;
registration
let X be left_end real-membered set;
cluster min X -> real;
coherence
proof
min X in X by Def7;
hence thesis;
end;
end;
registration
let X be left_end rational-membered set;
cluster min X -> rational;
coherence
proof
min X in X by Def7;
hence thesis;
end;
end;
registration
let X be left_end integer-membered set;
cluster min X -> integer;
coherence
proof
min X in X by Def7;
hence thesis;
end;
end;
registration
let X be left_end natural-membered set;
cluster min X -> natural;
coherence
proof
min X in X by Def7;
hence thesis;
end;
end;
registration
let X be right_end real-membered set;
cluster max X -> real;
coherence
proof
max X in X by Def8;
hence thesis;
end;
end;
registration
let X be right_end rational-membered set;
cluster max X -> rational;
coherence
proof
max X in X by Def8;
hence thesis;
end;
end;
registration
let X be right_end integer-membered set;
cluster max X -> integer;
coherence
proof
max X in X by Def8;
hence thesis;
end;
end;
registration
let X be right_end natural-membered set;
cluster max X -> natural;
coherence
proof
max X in X by Def8;
hence thesis;
end;
end;
registration
cluster left_end -> bounded_below for real-membered set;
coherence
proof
let X be real-membered set;
assume inf X in X;
then reconsider r = inf X as Real;
take r;
let x;
thus thesis by Th3;
end;
cluster right_end -> bounded_above for real-membered set;
coherence
proof
let X be real-membered set;
assume sup X in X;
then reconsider r = sup X as Real;
take r;
let x;
thus thesis by Th4;
end;
end;
theorem Th17:
x is LowerBound of [.x,y.]
proof
let z;
assume z in [.x,y.];
hence thesis by XXREAL_1:1;
end;
theorem Th18:
x is LowerBound of ].x,y.]
proof
let z;
assume z in ].x,y.];
hence thesis by XXREAL_1:2;
end;
theorem Th19:
x is LowerBound of [.x,y.[
proof
let z;
assume z in [.x,y.[;
hence thesis by XXREAL_1:3;
end;
theorem Th20:
x is LowerBound of ].x,y.[
proof
let z;
assume z in ].x,y.[;
hence thesis by XXREAL_1:4;
end;
theorem Th21:
y is UpperBound of [.x,y.]
proof
let z;
assume z in [.x,y.];
hence thesis by XXREAL_1:1;
end;
theorem Th22:
y is UpperBound of ].x,y.]
proof
let z;
assume z in ].x,y.];
hence thesis by XXREAL_1:2;
end;
theorem Th23:
y is UpperBound of [.x,y.[
proof
let z;
assume z in [.x,y.[;
hence thesis by XXREAL_1:3;
end;
theorem Th24:
y is UpperBound of ].x,y.[
proof
let z;
assume z in ].x,y.[;
hence thesis by XXREAL_1:4;
end;
theorem Th25:
x <= y implies inf [.x,y.] = x
proof
assume
A1: x <= y;
A2: for z being LowerBound of [.x,y.] holds z <= x
proof
let z be LowerBound of [.x,y.];
x in [.x,y.] by A1,XXREAL_1:1;
hence thesis by Def2;
end;
x is LowerBound of [.x,y.] by Th17;
hence thesis by A2,Def4;
end;
theorem Th26:
x < y implies inf [.x,y.[ = x
proof
assume
A1: x < y;
A2: for z being LowerBound of [.x,y.[ holds z <= x
proof
let z be LowerBound of [.x,y.[;
x in [.x,y.[ by A1,XXREAL_1:3;
hence thesis by Def2;
end;
x is LowerBound of [.x,y.[ by Th19;
hence thesis by A2,Def4;
end;
theorem Th27:
x < y implies inf ].x,y.] = x
proof
assume
A1: x < y;
A2: for z being LowerBound of ].x,y.] holds z <= x
proof
let z be LowerBound of ].x,y.];
for r st x < r & r < y holds z <= r
proof
let r;
assume that
A3: x < r and
A4: r < y;
r in ].x,y.] by A3,A4,XXREAL_1:2;
hence thesis by Def2;
end;
hence thesis by A1,XREAL_1:228;
end;
x is LowerBound of ].x,y.] by Th18;
hence thesis by A2,Def4;
end;
theorem Th28:
x < y implies inf ].x,y.[ = x
proof
assume
A1: x < y;
A2: for z being LowerBound of ].x,y.[ holds z <= x
proof
let z be LowerBound of ].x,y.[;
for r st x < r & r < y holds z <= r
by XXREAL_1:4,Def2;
hence thesis by A1,XREAL_1:228;
end;
x is LowerBound of ].x,y.[ by Th20;
hence thesis by A2,Def4;
end;
theorem Th29:
x <= y implies sup [.x,y.] = y
proof
assume
A1: x <= y;
A2: for z being UpperBound of [.x,y.] holds y <= z
proof
let z be UpperBound of [.x,y.];
y in [.x,y.] by A1,XXREAL_1:1;
hence thesis by Def1;
end;
y is UpperBound of [.x,y.] by Th21;
hence thesis by A2,Def3;
end;
theorem Th30:
x < y implies sup ].x,y.] = y
proof
assume
A1: x < y;
A2: for z being UpperBound of ].x,y.] holds y <= z
proof
let z be UpperBound of ].x,y.];
y in ].x,y.] by A1,XXREAL_1:2;
hence thesis by Def1;
end;
y is UpperBound of ].x,y.] by Th22;
hence thesis by A2,Def3;
end;
theorem Th31:
x < y implies sup [.x,y.[ = y
proof
assume
A1: x < y;
A2: for z being UpperBound of [.x,y.[ holds y <= z
proof
let z be UpperBound of [.x,y.[;
for r st x < r & r < y holds r <= z
proof
let r;
assume that
A3: x < r and
A4: r < y;
r in [.x,y.[ by A3,A4,XXREAL_1:3;
hence thesis by Def1;
end;
hence thesis by A1,XREAL_1:229;
end;
y is UpperBound of [.x,y.[ by Th23;
hence thesis by A2,Def3;
end;
theorem Th32:
x < y implies sup ].x,y.[ = y
proof
assume
A1: x < y;
A2: for z being UpperBound of ].x,y.[ holds y <= z
proof
let z be UpperBound of ].x,y.[;
for r st x < r & r < y holds r <= z
by XXREAL_1:4,Def1;
hence thesis by A1,XREAL_1:229;
end;
y is UpperBound of ].x,y.[ by Th24;
hence thesis by A2,Def3;
end;
theorem Th33:
x <= y implies [.x,y.] is left_end right_end
proof
assume
A1: x <= y;
then x in [.x,y.] by XXREAL_1:1;
then inf [.x,y.] in [.x,y.] by A1,Th25;
hence [.x,y.] is left_end;
y in [.x,y.] by A1,XXREAL_1:1;
hence sup [.x,y.] in [.x,y.] by A1,Th29;
end;
theorem Th34:
x < y implies [.x,y.[ is left_end
proof
assume
A1: x < y;
then x in [.x,y.[ by XXREAL_1:3;
hence inf [.x,y.[ in [.x,y.[ by A1,Th26;
end;
theorem Th35:
x < y implies ].x,y.] is right_end
proof
assume
A1: x < y;
then y in ].x,y.] by XXREAL_1:2;
hence sup ].x,y.] in ].x,y.] by A1,Th30;
end;
theorem Th36:
x is LowerBound of {}
proof
let y;
thus thesis;
end;
theorem Th37:
x is UpperBound of {}
proof
let y;
thus thesis;
end;
theorem Th38:
inf {} = +infty
proof
A1: for x being LowerBound of {} holds x <= +infty by XXREAL_0:3;
+infty is LowerBound of {} by Th36;
hence thesis by A1,Def4;
end;
theorem Th39:
sup {} = -infty
proof
A1: for x being UpperBound of {} holds -infty <= x by XXREAL_0:5;
-infty is UpperBound of {} by Th37;
hence thesis by A1,Def3;
end;
theorem Th40:
for X being ext-real-membered set holds X is non empty iff inf X <= sup X
proof
let X be ext-real-membered set;
thus X is non empty implies inf X <= sup X
proof
assume X is non empty;
then consider x such that
A1: x in X by MEMBERED:8;
A2: x <= sup X by A1,Th4;
inf X <= x by A1,Th3;
hence thesis by A2,XXREAL_0:2;
end;
assume inf X <= sup X;
hence thesis by Th38,Th39;
end;
registration
cluster real-bounded -> finite for integer-membered set;
coherence
proof
let X be integer-membered set;
per cases;
suppose
X is empty;
hence thesis;
end;
suppose
A1: X is non empty;
assume X is bounded_below bounded_above;
then reconsider Z = X as bounded_below bounded_above non empty
integer-membered set by A1;
set m = inf Z, n = sup Z;
defpred P[object] means $1 in X;
deffunc F(object) = $1;
set Y = {F(i) where i is Element of INT: m<=i & i<=n & P[i]};
A2: X c= Y
proof
let i be Integer;
A3: i in INT by INT_1:def 2;
assume
A4: P[i];
then
A5: i<=n by Th4;
m<=i by A4,Th3;
hence thesis by A3,A4,A5;
end;
Y is finite from FinInter;
hence thesis by A2;
end;
end;
end;
registration
cluster -> finite for bounded_above natural-membered set;
coherence;
end;
theorem
for X being ext-real-membered set holds +infty is UpperBound of X
proof
let X be ext-real-membered set;
let x such that
x in X;
thus thesis by XXREAL_0:3;
end;
theorem
for X being ext-real-membered set holds -infty is LowerBound of X
proof
let X be ext-real-membered set;
let x such that
x in X;
thus thesis by XXREAL_0:5;
end;
theorem Th43:
for X,Y being ext-real-membered set st X c= Y & Y is
bounded_above holds X is bounded_above
proof
let X,Y be ext-real-membered set;
assume
A1: X c= Y;
given r being Real such that
A2: r is UpperBound of Y;
take r;
thus thesis by A1,A2,Th6;
end;
theorem Th44:
for X,Y being ext-real-membered set st X c= Y & Y is
bounded_below holds X is bounded_below
proof
let X,Y be ext-real-membered set;
assume
A1: X c= Y;
given r being Real such that
A2: r is LowerBound of Y;
take r;
thus thesis by A1,A2,Th5;
end;
theorem
for X,Y being ext-real-membered set st X c= Y & Y is real-bounded holds
X is real-bounded
by Th43,Th44;
theorem Th46:
REAL is non bounded_below non bounded_above
proof
thus REAL is non bounded_below
proof
given r being Real such that
A1: r is LowerBound of REAL;
consider s being Real such that
A2: s < r by XREAL_1:2;
s in REAL by XREAL_0:def 1;
hence contradiction by A1,A2,Def2;
end;
given r being Real such that
A3: r is UpperBound of REAL;
consider s being Real such that
A4: r < s by XREAL_1:1;
s in REAL by XREAL_0:def 1;
hence contradiction by A3,A4,Def1;
end;
registration
cluster REAL -> non bounded_below non bounded_above;
coherence by Th46;
end;
theorem
{+infty} is bounded_below
proof
take 0;
let x;
assume x in {+infty};
hence thesis by TARSKI:def 1;
end;
theorem
{-infty} is bounded_above
proof
take 0;
let x;
assume x in {-infty};
hence thesis by TARSKI:def 1;
end;
theorem Th49:
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
proof
let X be bounded_above non empty ext-real-membered set;
assume X <> {-infty};
then consider x being object such that
A1: x in X and
A2: x <> -infty by ZFMISC_1:35;
reconsider x as ExtReal by A1;
consider r being Real such that
A3: r is UpperBound of X by Def10;
A4: r in REAL by XREAL_0:def 1;
x <= r by A3,A1,Def1;
then x in REAL by A4,A2,XXREAL_0:13;
hence thesis by A1;
end;
theorem Th50:
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
proof
let X be bounded_below non empty ext-real-membered set;
assume X <> {+infty};
then consider x being object such that
A1: x in X and
A2: x <> +infty by ZFMISC_1:35;
reconsider x as ExtReal by A1;
consider r being Real such that
A3: r is LowerBound of X by Def9;
A4: r in REAL by XREAL_0:def 1;
r <= x by A3,A1,Def2;
then x in REAL by A4,A2,XXREAL_0:10;
hence thesis by A1;
end;
theorem Th51:
for X being ext-real-membered set st -infty is UpperBound of X
holds X c= {-infty}
proof
let X be ext-real-membered set such that
A1: -infty is UpperBound of X;
let x;
assume x in X;
then x = -infty by A1,Def1,XXREAL_0:6;
hence thesis by TARSKI:def 1;
end;
theorem Th52:
for X being ext-real-membered set st +infty is LowerBound of X
holds X c= {+infty}
proof
let X be ext-real-membered set such that
A1: +infty is LowerBound of X;
let x;
assume x in X;
then x = +infty by A1,Def2,XXREAL_0:4;
hence thesis by TARSKI:def 1;
end;
theorem
for X being non empty ext-real-membered set st ex y being UpperBound
of X st y <> +infty holds X is bounded_above
proof
let X be non empty ext-real-membered set;
given y being UpperBound of X such that
A1: y <> +infty;
per cases;
suppose
A2: y = -infty;
take 0;
let x;
assume
A3: x in X;
X c= {-infty} by A2,Th51;
hence thesis by A3,TARSKI:def 1;
end;
suppose
y <> -infty;
then y in REAL by A1,XXREAL_0:14;
then reconsider y as Real;
take y;
thus thesis;
end;
end;
theorem
for X being non empty ext-real-membered set st ex y being LowerBound
of X st y <> -infty holds X is bounded_below
proof
let X be non empty ext-real-membered set;
given y being LowerBound of X such that
A1: y <> -infty;
per cases;
suppose
A2: y = +infty;
take 0;
let x;
assume
A3: x in X;
X c= {+infty} by A2,Th52;
hence thesis by A3,TARSKI:def 1;
end;
suppose
y <> +infty;
then y in REAL by A1,XXREAL_0:14;
then reconsider y as Real;
take y;
thus thesis;
end;
end;
theorem
for X being non empty ext-real-membered set, x being UpperBound of X
st x in X holds x = sup X
proof
let X be non empty ext-real-membered set, x be UpperBound of X;
assume x in X;
then for y being UpperBound of X holds x <= y by Def1;
hence thesis by Def3;
end;
theorem
for X being non empty ext-real-membered set, x being LowerBound of X
st x in X holds x = inf X
proof
let X be non empty ext-real-membered set, x be LowerBound of X;
assume x in X;
then for y being LowerBound of X holds y <= x by Def2;
hence thesis by Def4;
end;
theorem Th57:
for X being non empty ext-real-membered set st X is
bounded_above & X <> {-infty} holds sup X in REAL
proof
let X be non empty ext-real-membered set;
assume
A1: X is bounded_above;
then consider r being Real such that
A2: r is UpperBound of X;
assume X <> {-infty};
then
A3: ex x being Element of REAL st x in X by A1,Th49;
sup X is UpperBound of X by Def3;
then
A4: not sup X = -infty by A3,Def1,XXREAL_0:12;
A5: r in REAL by XREAL_0:def 1;
sup X <= r by A2,Def3;
hence thesis by A5,A4,XXREAL_0:13;
end;
theorem Th58:
for X being non empty ext-real-membered set st X is
bounded_below & X <> {+infty} holds inf X in REAL
proof
let X be non empty ext-real-membered set;
assume
A1: X is bounded_below;
then consider r being Real such that
A2: r is LowerBound of X;
assume X <> {+infty};
then
A3: ex x being Element of REAL st x in X by A1,Th50;
inf X is LowerBound of X by Def4;
then
A4: inf X <> +infty by A3,Def2,XXREAL_0:9;
A5: r in REAL by XREAL_0:def 1;
r <= inf X by A2,Def4;
hence thesis by A5,A4,XXREAL_0:10;
end;
theorem
for X,Y being ext-real-membered set st X c= Y holds sup X <= sup Y
proof
let X,Y be ext-real-membered set;
assume
A1: X c= Y;
sup Y is UpperBound of Y by Def3;
then sup Y is UpperBound of X by A1,Th6;
hence thesis by Def3;
end;
theorem
for X,Y being ext-real-membered set st X c= Y holds inf Y <= inf X
proof
let X,Y be ext-real-membered set;
assume
A1: X c= Y;
inf Y is LowerBound of Y by Def4;
then inf Y is LowerBound of X by A1,Th5;
hence thesis by Def4;
end;
theorem
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
proof
let X be ext-real-membered set;
let x be ExtReal;
given y being ExtReal such that
A1: y in X and
A2: x <= y;
y <= sup X by A1,Th4;
hence thesis by A2,XXREAL_0:2;
end;
theorem
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
proof
let X be ext-real-membered set;
let x be ExtReal;
given y being ExtReal such that
A1: y in X and
A2: y <= x;
inf X <= y by A1,Th3;
hence thesis by A2,XXREAL_0:2;
end;
theorem
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
proof
let X,Y be ext-real-membered set;
assume
A1: for x being ExtReal st x in X ex y being ExtReal st
y in Y & x <= y;
sup Y is UpperBound of X
proof
let x be ExtReal;
assume x in X;
then consider y being ExtReal such that
A2: y in Y and
A3: x <= y by A1;
y <= sup Y by A2,Th4;
hence thesis by A3,XXREAL_0:2;
end;
hence thesis by Def3;
end;
theorem
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
proof
let X,Y be ext-real-membered set;
assume
A1: for y being ExtReal st y in Y ex x being ExtReal st
x in X & x <= y;
inf X is LowerBound of Y
proof
let y be ExtReal;
assume y in Y;
then consider x being ExtReal such that
A2: x in X and
A3: x <= y by A1;
inf X <= x by A2,Th3;
hence thesis by A3,XXREAL_0:2;
end;
hence thesis by Def4;
end;
theorem Th65:
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
proof
let X,Y be ext-real-membered set, x be UpperBound of X, y be UpperBound of Y;
let a be ExtReal;
assume
A1: a in X /\ Y;
then a in Y by XBOOLE_0:def 4;
then
A2: a <= y by Def1;
a in X by A1,XBOOLE_0:def 4;
then a <= x by Def1;
hence thesis by A2,XXREAL_0:20;
end;
theorem Th66:
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
proof
let X,Y be ext-real-membered set, x be LowerBound of X, y be LowerBound of Y;
let a be ExtReal;
assume
A1: a in X /\ Y;
then a in Y by XBOOLE_0:def 4;
then
A2: y <= a by Def2;
a in X by A1,XBOOLE_0:def 4;
then x <= a by Def2;
hence thesis by A2,XXREAL_0:28;
end;
theorem
for X,Y being ext-real-membered set holds sup(X /\ Y) <= min(sup X,sup Y)
proof
let X,Y be ext-real-membered set;
A1: sup Y is UpperBound of Y by Def3;
sup X is UpperBound of X by Def3;
then min(sup X,sup Y) is UpperBound of X /\ Y by A1,Th65;
hence thesis by Def3;
end;
theorem
for X,Y being ext-real-membered set holds max(inf X,inf Y) <= inf(X /\ Y)
proof
let X,Y be ext-real-membered set;
A1: inf Y is LowerBound of Y by Def4;
inf X is LowerBound of X by Def4;
then max(inf X,inf Y) is LowerBound of X /\ Y by A1,Th66;
hence thesis by Def4;
end;
registration
cluster real-bounded -> real-membered for ext-real-membered set;
coherence
proof
let X be ext-real-membered set such that
A1: X is real-bounded;
let x be object;
assume
A2: x in X;
then reconsider X as non empty ext-real-membered set;
consider s being Real such that
A3: s is UpperBound of X by A1,Def10;
reconsider x as ExtReal by A2;
A4: s in REAL by XREAL_0:def 1;
A5: x <= s by A2,A3,Def1;
consider r being Real such that
A6: r is LowerBound of X by A1,Def9;
A7: r in REAL by XREAL_0:def 1;
r <= x by A2,A6,Def2;
then x in REAL by A5,A7,A4,XXREAL_0:45;
hence thesis;
end;
end;
theorem Th69:
A c= [.inf A, sup A.]
proof
let x be ExtReal;
assume
A1: x in A;
then
A2: x <= sup A by Th4;
inf A <= x by A1,Th3;
hence thesis by A2,XXREAL_1:1;
end;
theorem
sup A = inf A implies A = {inf A}
proof
assume
A1: sup A = inf A;
then A c= [.inf A,inf A.] by Th69;
then
A2: A c= {inf A} by XXREAL_1:17;
A <> {} by A1,Th38,Th39;
hence thesis by A2,ZFMISC_1:33;
end;
theorem Th71:
x <= y & x is UpperBound of A implies y is UpperBound of A
proof
assume that
A1: x <= y and
A2: x is UpperBound of A;
let z;
assume z in A;
then z <= x by A2,Def1;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th72:
y <= x & x is LowerBound of A implies y is LowerBound of A
proof
assume that
A1: y <= x and
A2: x is LowerBound of A;
let z;
assume z in A;
then x <= z by A2,Def2;
hence thesis by A1,XXREAL_0:2;
end;
theorem
A is bounded_above iff sup A <> +infty
proof
hereby
assume
A1: A is bounded_above;
per cases by A1,Th57;
suppose
A = {};
hence sup A <> +infty by Th39;
end;
suppose
A = {-infty};
hence sup A <> +infty by Lm1;
end;
suppose
sup A in REAL;
hence sup A <> +infty;
end;
end;
assume
A2: sup A <> +infty;
per cases by A2,XXREAL_0:14;
suppose
A3: sup A = -infty;
take 0;
-infty is UpperBound of A by A3,Def3;
hence thesis by Th71;
end;
suppose
sup A in REAL;
then reconsider r = sup A as Real;
take r;
thus thesis by Def3;
end;
end;
theorem
A is bounded_below iff inf A <> -infty
proof
hereby
assume
A1: A is bounded_below;
per cases by A1,Th58;
suppose
A = {};
hence inf A <> -infty by Th38;
end;
suppose
A = {+infty};
hence inf A <> -infty by Lm2;
end;
suppose
inf A in REAL;
hence inf A <> -infty;
end;
end;
assume
A2: inf A <> -infty;
per cases by A2,XXREAL_0:14;
suppose
A3: inf A = +infty;
take 0;
+infty is LowerBound of A by A3,Def4;
hence thesis by Th72;
end;
suppose
inf A in REAL;
then reconsider r = inf A as Real;
take r;
thus thesis by Def4;
end;
end;
begin :: Connectedness
definition
let A be ext-real-membered set;
attr A is interval means
:Def12:
for r,s being ExtReal st r in A & s in A holds [.r,s.] c= A;
end;
registration
cluster ExtREAL -> interval;
coherence
by MEMBERED:2;
cluster empty -> interval for ext-real-membered set;
coherence;
let r,s;
cluster [.r,s.] -> interval;
coherence
proof
let x,y;
assume x in [.r,s.];
then
A1: r <= x by XXREAL_1:1;
assume y in [.r,s.];
then
A2: y <= s by XXREAL_1:1;
let z;
assume
A3: z in [.x,y.];
then x <= z by XXREAL_1:1;
then
A4: r <= z by A1,XXREAL_0:2;
z <= y by A3,XXREAL_1:1;
then z <= s by A2,XXREAL_0:2;
hence thesis by A4,XXREAL_1:1;
end;
cluster ].r,s.] -> interval;
coherence
proof
let x,y;
assume x in ].r,s.];
then
A5: r < x by XXREAL_1:2;
assume y in ].r,s.];
then
A6: y <= s by XXREAL_1:2;
let z;
assume
A7: z in [.x,y.];
then x <= z by XXREAL_1:1;
then
A8: r < z by A5,XXREAL_0:2;
z <= y by A7,XXREAL_1:1;
then z <= s by A6,XXREAL_0:2;
hence thesis by A8,XXREAL_1:2;
end;
cluster [.r,s.[ -> interval;
coherence
proof
let x,y;
assume x in [.r,s.[;
then
A9: r <= x by XXREAL_1:3;
assume y in [.r,s.[;
then
A10: y < s by XXREAL_1:3;
let z;
assume
A11: z in [.x,y.];
then x <= z by XXREAL_1:1;
then
A12: r <= z by A9,XXREAL_0:2;
z <= y by A11,XXREAL_1:1;
then z < s by A10,XXREAL_0:2;
hence thesis by A12,XXREAL_1:3;
end;
cluster ].r,s.[ -> interval;
coherence
proof
let x,y;
assume x in ].r,s.[;
then
A13: r < x by XXREAL_1:4;
assume y in ].r,s.[;
then
A14: y < s by XXREAL_1:4;
let z;
assume
A15: z in [.x,y.];
then x <= z by XXREAL_1:1;
then
A16: r < z by A13,XXREAL_0:2;
z <= y by A15,XXREAL_1:1;
then z < s by A14,XXREAL_0:2;
hence thesis by A16,XXREAL_1:4;
end;
end;
registration
cluster REAL -> interval;
coherence by XXREAL_1:224;
end;
registration
cluster interval for non empty ext-real-membered set;
existence
proof
take REAL;
thus thesis;
end;
end;
registration
let A,B be interval ext-real-membered set;
cluster A /\ B -> interval;
coherence
proof
let r,s be ExtReal;
assume that
A1: r in A /\ B and
A2: s in A /\ B;
A3: s in B by A2,XBOOLE_0:def 4;
r in B by A1,XBOOLE_0:def 4;
then
A4: [.r,s.] c= B by A3,Def12;
A5: s in A by A2,XBOOLE_0:def 4;
r in A by A1,XBOOLE_0:def 4;
then [.r,s.] c= A by A5,Def12;
hence thesis by A4,XBOOLE_1:19;
end;
end;
reserve A,B for ext-real-membered set;
registration
let r,s;
cluster ].r,s.] -> non left_end;
coherence
proof
assume ].r,s.] is left_end;
then
A1: inf ].r,s.] in ].r,s.];
then
A2: inf ].r,s.] <= s by XXREAL_1:2;
r < inf ].r,s.] by A1,XXREAL_1:2;
then r < s by A2,XXREAL_0:2;
then r = inf ].r,s.] by Th27;
hence contradiction by A1,XXREAL_1:2;
end;
cluster [.r,s.[ -> non right_end;
coherence
proof
assume [.r,s.[ is right_end;
then
A3: sup [.r,s.[ in [.r,s.[;
then
A4: sup [.r,s.[ < s by XXREAL_1:3;
r <= sup [.r,s.[ by A3,XXREAL_1:3;
then r < s by A4,XXREAL_0:2;
then s = sup [.r,s.[ by Th31;
hence contradiction by A3,XXREAL_1:3;
end;
cluster ].r,s.[ -> non left_end non right_end;
coherence
proof
thus ].r,s.[ is non left_end
proof
assume ].r,s.[ is left_end;
then
A5: inf ].r,s.[ in ].r,s.[;
then
A6: inf ].r,s.[ < s by XXREAL_1:4;
r < inf ].r,s.[ by A5,XXREAL_1:4;
then r < s by A6,XXREAL_0:2;
then r = inf ].r,s.[ by Th28;
hence contradiction by A5,XXREAL_1:4;
end;
assume ].r,s.[ is right_end;
then
A7: sup ].r,s.[ in ].r,s.[;
then
A8: sup ].r,s.[ < s by XXREAL_1:4;
r < sup ].r,s.[ by A7,XXREAL_1:4;
then r < s by A8,XXREAL_0:2;
then s = sup ].r,s.[ by Th32;
hence contradiction by A7,XXREAL_1:4;
end;
end;
registration
cluster left_end right_end interval for ext-real-membered set;
existence
proof
take [.0,1.];
thus thesis by Th33;
end;
cluster non left_end right_end interval for ext-real-membered set;
existence
proof
take ].0,1.];
thus thesis by Th35;
end;
cluster left_end non right_end interval for ext-real-membered set;
existence
proof
take [.0,1.[;
thus thesis by Th34;
end;
cluster non left_end non right_end interval non empty for ext-real-membered
set;
existence
proof
take ].0,2.[;
1 in ].0,2.[ by XXREAL_1:4;
hence thesis;
end;
end;
theorem
for A being left_end right_end interval ext-real-membered set holds
A = [.min A, max A.]
proof
let A be left_end right_end interval ext-real-membered set;
let x;
A1: max A in A by Def6;
thus x in A implies x in [.min A, max A.]
proof
assume
A2: x in A;
then
A3: x <= max A by Th4;
min A <= x by A2,Th3;
hence thesis by A3,XXREAL_1:1;
end;
min A in A by Def5;
then [.min A, max A.] c= A by A1,Def12;
hence thesis;
end;
theorem
for A being non left_end right_end interval ext-real-membered set
holds A = ].inf A, max A.]
proof
let A be non left_end right_end interval ext-real-membered set;
let x;
defpred P[ExtReal] means $1 in A & $1 < x;
thus x in A implies x in ].inf A, max A.]
proof
A1: not inf A in A by Def5;
assume
A2: x in A;
then
A3: x <= max A by Th4;
inf A <= x by A2,Th3;
then inf A < x by A2,A1,XXREAL_0:1;
hence thesis by A3,XXREAL_1:2;
end;
assume
A4: x in ].inf A, max A.];
per cases;
suppose
not ex r st P[r];
then x is LowerBound of A by Def2;
then x <= inf A by Def4;
hence thesis by A4,XXREAL_1:2;
end;
suppose
ex r st P[r];
then consider r such that
A5: r in A and
A6: r < x;
x <= max A by A4,XXREAL_1:2;
then
A7: x in [.r,max A.] by A6,XXREAL_1:1;
max A in A by Def6;
then [.r,max A.] c= A by A5,Def12;
hence thesis by A7;
end;
end;
theorem
for A being left_end non right_end interval ext-real-membered set
holds A = [.min A, sup A.[
proof
let A be left_end non right_end interval ext-real-membered set;
let x;
defpred P[ExtReal] means $1 in A & $1 > x;
thus x in A implies x in [.min A, sup A.[
proof
A1: not sup A in A by Def6;
assume
A2: x in A;
then
A3: min A <= x by Th3;
x <= sup A by A2,Th4;
then x < sup A by A2,A1,XXREAL_0:1;
hence thesis by A3,XXREAL_1:3;
end;
assume
A4: x in [.min A, sup A.[;
per cases;
suppose
not ex r st P[r];
then x is UpperBound of A by Def1;
then sup A <= x by Def3;
hence thesis by A4,XXREAL_1:3;
end;
suppose
ex r st P[r];
then consider r such that
A5: r in A and
A6: r > x;
inf A <= x by A4,XXREAL_1:3;
then
A7: x in [.inf A,r.] by A6,XXREAL_1:1;
min A in A by Def5;
then [.inf A,r.] c= A by A5,Def12;
hence thesis by A7;
end;
end;
theorem Th78:
for A being non left_end non right_end non empty interval
ext-real-membered set holds A =].inf A,sup A.[
proof
let A be non left_end non right_end non empty interval ext-real-membered
set;
let x;
defpred P[ExtReal] means $1 in A & $1 < x;
defpred Q[ExtReal] means $1 in A & $1 > x;
thus x in A implies x in ].inf A,sup A.[
proof
assume
A1: x in A;
then
A2: x <> sup A by Def6;
x <= sup A by A1,Th4;
then
A3: x < sup A by A2,XXREAL_0:1;
A4: x <> inf A by A1,Def5;
inf A <= x by A1,Th3;
then inf A < x by A4,XXREAL_0:1;
hence thesis by A3,XXREAL_1:4;
end;
assume
A5: x in ].inf A,sup A.[;
per cases;
suppose
not ex r st P[r];
then x is LowerBound of A by Def2;
then x <= inf A by Def4;
hence thesis by A5,XXREAL_1:4;
end;
suppose
not ex r st Q[r];
then x is UpperBound of A by Def1;
then sup A <= x by Def3;
hence thesis by A5,XXREAL_1:4;
end;
suppose that
A6: ex r st P[r] and
A7: ex r st Q[r];
consider r such that
A8: r in A and
A9: r < x by A6;
consider s such that
A10: s in A and
A11: s > x by A7;
A12: x in [.r,s.] by A9,A11,XXREAL_1:1;
[.r,s.] c= A by A8,A10,Def12;
hence thesis by A12;
end;
end;
theorem
for A being non left_end non right_end interval ext-real-membered
set ex r,s st r <= s & A =].r,s.[
proof
let A be non left_end non right_end interval ext-real-membered set;
per cases;
suppose
A1: A is empty;
take -infty,-infty;
thus thesis by A1;
end;
suppose
A2: A is not empty;
take inf A, sup A;
thus inf A <= sup A by A2,Th40;
thus thesis by A2,Th78;
end;
end;
theorem Th80:
A is interval implies for x,y,r st x in A & y in A & x <= r & r
<= y holds r in A
proof
assume
A1: A is interval;
let x,y,r such that
A2: x in A and
A3: y in A and
A4: x <= r and
A5: r <= y;
A6: r in [.x,y.] by A4,A5,XXREAL_1:1;
[.x,y.] c= A by A1,A2,A3;
hence thesis by A6;
end;
theorem Th81:
A is interval implies for x,r st x in A & x <= r & r < sup A holds r in A
proof
assume
A1: A is interval;
let x,r such that
A2: x in A and
A3: x <= r and
A4: r < sup A;
per cases;
suppose
ex y st y in A & r < y;
hence thesis by A1,A2,A3,Th80;
end;
suppose
not ex y st y in A & r < y;
then r is UpperBound of A by Def1;
hence thesis by A4,Def3;
end;
end;
theorem Th82:
A is interval implies for x,r st x in A & inf A < r & r <= x holds r in A
proof
assume
A1: A is interval;
let x,r such that
A2: x in A and
A3: inf A < r and
A4: r <= x;
per cases;
suppose
ex y st y in A & r > y;
hence thesis by A1,A2,A4,Th80;
end;
suppose
not ex y st y in A & r > y;
then r is LowerBound of A by Def2;
hence thesis by A3,Def4;
end;
end;
theorem
A is interval implies for r st inf A < r & r < sup A holds r in A
proof
assume
A1: A is interval;
let r such that
A2: inf A < r and
A3: r < sup A;
per cases;
suppose
ex y st y in A & r > y;
hence thesis by A1,A3,Th81;
end;
suppose
not ex y st y in A & r > y;
then r is LowerBound of A by Def2;
hence thesis by A2,Def4;
end;
end;
theorem Th84:
(for x,y,r st x in A & y in A & x < r & r < y holds r in A)
implies A is interval
proof
assume
A1: for x,y,r st x in A & y in A & x < r & r < y holds r in A;
let x,y such that
A2: x in A and
A3: y in A;
let r;
assume r in [.x,y.];
then r in ].x,y.[ \/ {x,y} by XXREAL_1:29,128;
then
A4: r in ].x,y.[ or r in {x,y} by XBOOLE_0:def 3;
per cases by A4,TARSKI:def 2;
suppose
r = x;
hence thesis by A2;
end;
suppose
r = y;
hence thesis by A3;
end;
suppose
A5: r in ].x,y.[;
then
A6: r < y by XXREAL_1:4;
x < r by A5,XXREAL_1:4;
hence thesis by A1,A2,A3,A6;
end;
end;
theorem
(for x,r st x in A & x < r & r < sup A holds r in A) implies A is interval
proof
assume
A1: for x,r st x in A & x < r & r < sup A holds r in A;
let x,y such that
A2: x in A and
A3: y in A;
let r;
assume r in [.x,y.];
then r in ].x,y.[ \/ {x,y} by XXREAL_1:29,128;
then
A4: r in ].x,y.[ or r in {x,y} by XBOOLE_0:def 3;
per cases by A4,TARSKI:def 2;
suppose
r = x;
hence thesis by A2;
end;
suppose
r = y;
hence thesis by A3;
end;
suppose
A5: r in ].x,y.[;
then
A6: r < y by XXREAL_1:4;
y <= sup A by A3,Th4;
then
A7: r < sup A by A6,XXREAL_0:2;
x < r by A5,XXREAL_1:4;
hence thesis by A1,A2,A7;
end;
end;
theorem
(for y,r st y in A & inf A < r & r < y holds r in A) implies A is interval
proof
assume
A1: for y,r st y in A & inf A < r & r < y holds r in A;
let x,y such that
A2: x in A and
A3: y in A;
let r;
assume r in [.x,y.];
then r in ].x,y.[ \/ {x,y} by XXREAL_1:29,128;
then
A4: r in ].x,y.[ or r in {x,y} by XBOOLE_0:def 3;
per cases by A4,TARSKI:def 2;
suppose
r = x;
hence thesis by A2;
end;
suppose
r = y;
hence thesis by A3;
end;
suppose
A5: r in ].x,y.[;
then
A6: x < r by XXREAL_1:4;
inf A <= x by A2,Th3;
then
A7: inf A < r by A6,XXREAL_0:2;
r < y by A5,XXREAL_1:4;
hence thesis by A1,A3,A7;
end;
end;
theorem
(for r st inf A < r & r < sup A holds r in A) implies A is interval
proof
assume
A1: for r st inf A < r & r < sup A holds r in A;
let x,y such that
A2: x in A and
A3: y in A;
let r;
assume r in [.x,y.];
then r in ].x,y.[ \/ {x,y} by XXREAL_1:29,128;
then
A4: r in ].x,y.[ or r in {x,y} by XBOOLE_0:def 3;
per cases by A4,TARSKI:def 2;
suppose
r = x;
hence thesis by A2;
end;
suppose
r = y;
hence thesis by A3;
end;
suppose
A5: r in ].x,y.[;
then
A6: r < y by XXREAL_1:4;
y <= sup A by A3,Th4;
then
A7: r < sup A by A6,XXREAL_0:2;
A8: x < r by A5,XXREAL_1:4;
inf A <= x by A2,Th3;
then inf A < r by A8,XXREAL_0:2;
hence thesis by A1,A7;
end;
end;
theorem Th88:
(for x,y,r st x in A & y in A & x <= r & r <= y holds r in A)
implies A is interval
proof
assume for x,y,r st x in A & y in A & x <= r & r <= y holds r in A;
then for x,y,r st x in A & y in A & x < r & r < y holds r in A;
hence thesis by Th84;
end;
theorem
A is interval & B is interval & A meets B implies A \/ B is interval
proof
assume that
A1: A is interval and
A2: B is interval;
given z such that
A3: z in A and
A4: z in B;
for x,y,r st x in A \/ B & y in A \/ B & x <= r & r <= y holds r in A \/ B
proof
let x,y,r such that
A5: x in A \/ B and
A6: y in A \/ B and
A7: x <= r and
A8: r <= y;
per cases by A5,A6,XBOOLE_0:def 3;
suppose
x in A & y in A;
then r in A by A1,A7,A8,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A9: x in A and
A10: y in B;
per cases;
suppose
r <= z;
then r in A by A1,A3,A7,A9,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose
z <= r;
then r in B by A2,A4,A8,A10,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
suppose that
A11: x in B and
A12: y in A;
per cases;
suppose
z <= r;
then r in A by A1,A3,A8,A12,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose
r <= z;
then r in B by A2,A4,A7,A11,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
suppose
x in B & y in B;
then r in B by A2,A7,A8,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by Th88;
end;
theorem
A is interval & B is left_end interval & sup A = inf B implies A \/
B is interval
proof
assume that
A1: A is interval and
A2: B is left_end interval and
A3: sup A = inf B;
set z = inf B;
for x,y,r st x in A \/ B & y in A \/ B & x < r & r < y holds r in A \/ B
proof
let x,y,r such that
A4: x in A \/ B and
A5: y in A \/ B and
A6: x < r and
A7: r < y;
per cases by A4,A5,XBOOLE_0:def 3;
suppose
x in A & y in A;
then r in A by A1,A6,A7,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A8: x in A and
A9: y in B;
per cases;
suppose
r < z;
then r in A by A1,A3,A6,A8,Th81;
hence thesis by XBOOLE_0:def 3;
end;
suppose
z <= r;
then r in B by A2,A7,A9,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
suppose that
A10: x in B and
A11: y in A;
per cases;
suppose
A12: z < r;
y <= z by A3,A11,Th4;
hence thesis by A7,A12,XXREAL_0:2;
end;
suppose
r <= z;
then r in B by A2,A6,A10,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
suppose
x in B & y in B;
then r in B by A2,A6,A7,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by Th84;
end;
theorem
A is right_end interval & B is interval & sup A = inf B implies A \/
B is interval
proof
assume that
A1: A is right_end interval and
A2: B is interval and
A3: sup A = inf B;
set z = inf B;
A4: z in A by A1,A3;
for x,y,r st x in A \/ B & y in A \/ B & x < r & r < y holds r in A \/ B
proof
let x,y,r such that
A5: x in A \/ B and
A6: y in A \/ B and
A7: x < r and
A8: r < y;
per cases by A5,A6,XBOOLE_0:def 3;
suppose
x in A & y in A;
then r in A by A1,A7,A8,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose that
A9: x in A and
A10: y in B;
per cases;
suppose
r <= z;
then r in A by A1,A4,A7,A9,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose
z < r;
then r in B by A2,A8,A10,Th82;
hence thesis by XBOOLE_0:def 3;
end;
end;
suppose that
A11: x in B and
A12: y in A;
per cases;
suppose
z <= r;
then r in A by A1,A4,A8,A12,Th80;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A13: r < z;
z <= x by A11,Th3;
hence thesis by A7,A13,XXREAL_0:2;
end;
end;
suppose
x in B & y in B;
then r in B by A2,A7,A8,Th80;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by Th84;
end;
registration
cluster left_end -> non empty for ext-real-membered set;
coherence;
cluster right_end -> non empty for ext-real-membered set;
coherence;
end;
:: from HAHNBAN, 2011.04.26, A.T.
theorem
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}
proof
let A be non empty Subset of ExtREAL such that
A1: for r being Element of ExtREAL st r in A holds r <= -infty;
assume A <> {-infty};
then ex a being Element of A st a <> -infty by SETFAM_1:49;
hence contradiction by A1,XXREAL_0:6;
end;
theorem
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}
proof
let A be non empty Subset of ExtREAL such that
A1: for r being Element of ExtREAL st r in A holds +infty <= r;
assume A <> {+infty};
then ex a being Element of A st a <> +infty by SETFAM_1:49;
hence contradiction by A1,XXREAL_0:4;
end;
theorem Th94:
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
proof
let A be non empty Subset of ExtREAL, r be ExtReal;
assume
A1: r < sup A;
assume
A2: for s being Element of ExtREAL st s in A holds not r < s;
r is UpperBound of A
proof
let x be ExtReal;
assume x in A;
hence thesis by A2;
end;
hence contradiction by A1,Def3;
end;
theorem Th95:
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
proof
let A be non empty Subset of ExtREAL, r be Element of ExtREAL;
assume
A1: inf A < r;
assume
A2: for s being Element of ExtREAL st s in A holds not s < r;
r is LowerBound of A
proof
let x be ExtReal;
thus thesis by A2;
end;
hence contradiction by A1,Def4;
end;
theorem
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
proof
let A,B be non empty Subset of ExtREAL;
assume
A1: for r,s being ExtReal st r in A & s in B holds r <= s;
assume not sup A <= inf B;
then consider s1 being Element of ExtREAL such that
A2: s1 in A and
A3: inf B < s1 by Th94;
ex s2 being Element of ExtREAL st s2 in B & s2 < s1 by A3,Th95;
hence contradiction by A1,A2;
end;