:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-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 SUBSET_1, NUMBERS, XXREAL_0, MEMBERED, XXREAL_2, ORDINAL1,
XBOOLE_0, TARSKI, ORDINAL2, SETFAM_1, ZFMISC_1, SUPINF_1;
notations XBOOLE_0, SUBSET_1, ZFMISC_1, SETFAM_1, DOMAIN_1, ORDINAL1, NUMBERS,
MEMBERED, XXREAL_0, XXREAL_2;
constructors NUMBERS, XXREAL_0, XREAL_0, MEMBERED, SETFAM_1, DOMAIN_1,
XXREAL_2;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, MEMBERED;
requirements SUBSET, BOOLE;
definitions MEMBERED, SETFAM_1;
expansions MEMBERED;
theorems TARSKI, XXREAL_0, SETFAM_1, XXREAL_2;
schemes MEMBERED;
begin
definition
mode R_eal is Element of ExtREAL;
end;
definition
redefine func +infty -> R_eal; :: redefines +infty (XXREAL_0, definition)
coherence by XXREAL_0:def 1;
redefine func -infty -> R_eal; :: redefines -infty (XXREAL_0, definition)
coherence by XXREAL_0:def 1;
end;
::
:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL
::
definition
let X be ext-real-membered set;
func SetMajorant(X) -> ext-real-membered set means
:Def1:
for x being ExtReal holds x in it iff x is UpperBound of X;
existence
proof
defpred P[ExtReal] means $1 is UpperBound of X;
consider Y being ext-real-membered set such that
A1: for x being ExtReal holds x in Y iff P[x] from MEMBERED:
sch 2;
take Y;
thus thesis by A1;
end;
uniqueness
proof
let Y1,Y2 be ext-real-membered set such that
A2: for x being ExtReal holds x in Y1 iff x is UpperBound of X and
A3: for x being ExtReal holds x in Y2 iff x is UpperBound of X;
let x be ExtReal;
x in Y1 iff x is UpperBound of X by A2;
hence thesis by A3;
end;
end;
registration
let X be ext-real-membered set;
cluster SetMajorant(X) -> non empty;
coherence
proof
set x = the UpperBound of X;
x in SetMajorant(X) by Def1;
hence thesis;
end;
end;
theorem
for X,Y being ext-real-membered set st X c= Y holds for x being
ExtReal holds x in SetMajorant Y implies x in SetMajorant(X)
proof
let X,Y be ext-real-membered set;
assume
A1: X c= Y;
let x be ExtReal;
assume x in SetMajorant(Y);
then x is UpperBound of Y by Def1;
then x is UpperBound of X by A1,XXREAL_2:6;
hence thesis by Def1;
end;
definition
let X be ext-real-membered set;
func SetMinorant(X) -> ext-real-membered set means
:Def2:
for x being ExtReal holds x in it iff x is LowerBound of X;
existence
proof
defpred P[ExtReal] means $1 is LowerBound of X;
consider Y being ext-real-membered set such that
A1: for x being ExtReal holds x in Y iff P[x] from MEMBERED:
sch 2;
take Y;
thus thesis by A1;
end;
uniqueness
proof
let Y1,Y2 be ext-real-membered set such that
A2: for x being ExtReal holds x in Y1 iff x is LowerBound of X and
A3: for x being ExtReal holds x in Y2 iff x is LowerBound of X;
let x be ExtReal;
x in Y1 iff x is LowerBound of X by A2;
hence thesis by A3;
end;
end;
registration
let X be ext-real-membered set;
cluster SetMinorant(X) -> non empty;
coherence
proof
set x = the LowerBound of X;
x in SetMinorant(X) by Def2;
hence thesis;
end;
end;
theorem
for X,Y being ext-real-membered set st X c= Y holds for x being
ExtReal holds x in SetMinorant(Y) implies x in SetMinorant(X)
proof
let X,Y be ext-real-membered set;
assume
A1: X c= Y;
let x be ExtReal;
assume x in SetMinorant(Y);
then x is LowerBound of Y by Def2;
then x is LowerBound of X by A1,XXREAL_2:5;
hence thesis by Def2;
end;
::
:: sup X, inf X least upper bound and greatest lower bound of set X
::
theorem
for X being non empty ext-real-membered set holds sup X = inf
SetMajorant(X) & inf X = sup SetMinorant(X)
proof
let X be non empty ext-real-membered set;
for y being ExtReal st y in SetMajorant X holds sup X <= y
proof
let y be ExtReal;
assume y in SetMajorant X;
then y is UpperBound of X by Def1;
hence thesis by XXREAL_2:def 3;
end;
then
A1: sup X is LowerBound of SetMajorant X by XXREAL_2:def 2;
inf X is LowerBound of X by XXREAL_2:def 4;
then
A2: inf X in SetMinorant X by Def2;
for y being ExtReal st y in SetMinorant X holds y <= inf X
proof
let y be ExtReal;
assume y in SetMinorant X;
then y is LowerBound of X by Def2;
hence thesis by XXREAL_2:def 4;
end;
then
A3: inf X is UpperBound of SetMinorant X by XXREAL_2:def 1;
sup X is UpperBound of X by XXREAL_2:def 3;
then sup X in SetMajorant X by Def1;
hence thesis by A1,A2,A3,XXREAL_2:55,56;
end;
registration
let X be non empty set;
cluster non empty with_non-empty_elements for Subset-Family of X;
existence
proof
take {[#]X};
thus {[#]X} is non empty;
assume {} in {[#]X};
hence contradiction by TARSKI:def 1;
end;
end;
definition
let X be non empty set;
mode bool_DOMAIN of X is non empty with_non-empty_elements Subset-Family of
X;
end;
definition
let F be bool_DOMAIN of ExtREAL;
func SUP(F) -> ext-real-membered set means
:Def3:
for a being ExtReal
holds a in it iff ex A being non empty ext-real-membered set st A in F &
a = sup A;
existence
proof
defpred P[ExtReal] means ex A being non empty ext-real-membered
set st A in F & $1 = sup A;
consider S being ext-real-membered set such that
A1: for a being ExtReal holds a in S iff P[a] from MEMBERED:
sch 2;
reconsider S as ext-real-membered set;
take S;
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be ext-real-membered set such that
A2: for a being ExtReal holds a in S1 iff ex A being non empty
ext-real-membered set st A in F & a = sup A and
A3: for a being ExtReal holds a in S2 iff ex A being non empty
ext-real-membered set st A in F & a = sup A;
let a be ExtReal;
hereby
assume a in S1;
then
ex A being non empty ext-real-membered set st A in F & a = sup A by A2;
hence a in S2 by A3;
end;
assume a in S2;
then
ex A being non empty ext-real-membered set st A in F & a = sup A by A3;
hence thesis by A2;
end;
end;
registration
let F be bool_DOMAIN of ExtREAL;
cluster SUP(F) -> non empty;
coherence
proof
set A = the Element of F;
reconsider A as non empty ext-real-membered set by SETFAM_1:def 8;
sup A = sup A;
hence thesis by Def3;
end;
end;
theorem Th4:
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered number st S = union F holds sup S is UpperBound of SUP(F)
proof
let F be bool_DOMAIN of ExtREAL, S be non empty ext-real-membered set;
assume
A1: S = union F;
for x being ExtReal st x in SUP(F) holds x <= sup S
proof
let x be ExtReal;
assume x in SUP(F);
then consider A being non empty ext-real-membered set such that
A2: A in F and
A3: x = sup A by Def3;
A c= S
by A1,A2,TARSKI:def 4;
hence thesis by A3,XXREAL_2:59;
end;
hence thesis by XXREAL_2:def 1;
end;
theorem Th5:
for F being bool_DOMAIN of ExtREAL, S being ext-real-membered
set st S = union F holds sup SUP(F) is UpperBound of S
proof
let F be bool_DOMAIN of ExtREAL, S be ext-real-membered set;
assume
A1: S = union F;
for x being ExtReal st x in S holds x <= sup SUP(F)
proof
let x be ExtReal;
assume x in S;
then consider Z being set such that
A2: x in Z and
A3: Z in F by A1,TARSKI:def 4;
reconsider Z as non empty ext-real-membered set by A2,A3;
set a = sup Z;
sup Z is UpperBound of Z & a in SUP(F) by A3,Def3,XXREAL_2:def 3;
hence thesis by A2,XXREAL_2:61,def 1;
end;
hence thesis by XXREAL_2:def 1;
end;
theorem
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered set st S = union F holds sup S = sup SUP(F)
proof
let F be bool_DOMAIN of ExtREAL, S be non empty ext-real-membered set;
set a = sup S;
set b = sup SUP(F);
assume
A1: S = union F;
then sup S is UpperBound of SUP(F) by Th4;
then
A2: b <= a by XXREAL_2:def 3;
sup SUP(F) is UpperBound of S by A1,Th5;
then a <= b by XXREAL_2:def 3;
hence thesis by A2,XXREAL_0:1;
end;
definition
let F be bool_DOMAIN of ExtREAL;
func INF F -> ext-real-membered set means
:Def4:
for a being ExtReal
holds a in it iff ex A being non empty ext-real-membered set st A in F &
a = inf A;
existence
proof
set A = the Element of F;
defpred P[ExtReal] means ex A being non empty ext-real-membered
set st A in F & $1 = inf A;
reconsider A as non empty ext-real-membered set by SETFAM_1:def 8;
consider S being ext-real-membered set such that
A1: for a being ExtReal holds a in S iff P[a] from MEMBERED:
sch 2;
inf A = inf A;
then reconsider S as non empty ext-real-membered set by A1;
take S;
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be ext-real-membered set such that
A2: for a being ExtReal holds a in S1 iff ex A being non empty
ext-real-membered set st A in F & a = inf A and
A3: for a being ExtReal holds a in S2 iff ex A being non empty
ext-real-membered set st A in F & a = inf A;
for a being object holds a in S1 iff a in S2
proof
let a be object;
hereby
assume
A4: a in S1;
then reconsider a9 = a as ExtReal;
ex A being non empty ext-real-membered set st A in F & a9 = inf A
by A2,A4;
hence a in S2 by A3;
end;
assume
A5: a in S2;
then reconsider a as ExtReal;
ex A being non empty ext-real-membered set st A in F & a = inf A by A3,A5
;
hence thesis by A2;
end;
hence thesis;
end;
end;
registration
let F be bool_DOMAIN of ExtREAL;
cluster INF(F) -> non empty;
coherence
proof
set A = the Element of F;
reconsider A as non empty ext-real-membered set by SETFAM_1:def 8;
inf A = inf A;
hence thesis by Def4;
end;
end;
theorem Th7:
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered set st S = union F holds inf S is LowerBound of INF(F)
proof
let F be bool_DOMAIN of ExtREAL, S be non empty ext-real-membered set;
assume
A1: S = union F;
for x being ExtReal st x in INF(F) holds inf S <= x
proof
let x be ExtReal;
assume x in INF(F);
then consider A being non empty ext-real-membered set such that
A2: A in F and
A3: x = inf A by Def4;
A c= S
by A1,A2,TARSKI:def 4;
hence thesis by A3,XXREAL_2:60;
end;
hence thesis by XXREAL_2:def 2;
end;
theorem Th8:
for F being bool_DOMAIN of ExtREAL, S being ext-real-membered
set st S = union F holds inf INF(F) is LowerBound of S
proof
let F be bool_DOMAIN of ExtREAL, S be ext-real-membered set;
assume
A1: S = union F;
for x being ExtReal st x in S holds inf INF(F) <= x
proof
let x be ExtReal;
assume x in S;
then consider Z being set such that
A2: x in Z and
A3: Z in F by A1,TARSKI:def 4;
reconsider Z as non empty ext-real-membered set by A2,A3;
set a = inf Z;
inf Z is LowerBound of Z & a in INF(F) by A3,Def4,XXREAL_2:def 4;
hence thesis by A2,XXREAL_2:62,def 2;
end;
hence thesis by XXREAL_2:def 2;
end;
theorem
for F being bool_DOMAIN of ExtREAL, S being non empty
ext-real-membered set st S = union F holds inf S = inf INF(F)
proof
let F be bool_DOMAIN of ExtREAL, S be non empty ext-real-membered set;
set a = inf S;
set b = inf INF(F);
assume
A1: S = union F;
then inf S is LowerBound of INF(F) by Th7;
then
A2: a <= b by XXREAL_2:def 4;
inf INF(F) is LowerBound of S by A1,Th8;
then b <= a by XXREAL_2:def 4;
hence thesis by A2,XXREAL_0:1;
end;