:: MEASURE5 semantic presentation

REAL is non empty V5() V36() complex-membered ext-real-membered real-membered V47() non bounded_below non bounded_above interval set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below Element of K32(REAL)
K32(REAL) is non empty set
ExtREAL is non empty ext-real-membered interval set
K33(NAT,ExtREAL) is set
K32(K33(NAT,ExtREAL)) is non empty set
K32(ExtREAL) is non empty set
omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below set
K32(omega) is non empty set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
{+infty,-infty} is non empty V36() ext-real-membered left_end right_end set
REAL \/ {+infty,-infty} is non empty ext-real-membered set
{} is empty V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval set
the empty V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval set is empty V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval set
].-infty,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not +infty <= b₁ ) } is set
0 is empty natural V24() real ext-real non positive non negative V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval Element of NAT
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
a is complex-membered ext-real-membered real-membered Element of K32(REAL)
b is V24() real ext-real set
a is ext-real Element of ExtREAL
b is V24() real ext-real set
a is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
].X,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= X & not a <= b₁ ) } is set
].X,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
b is set
b is complex-membered ext-real-membered real-membered Element of K32(REAL)
].X,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
a is V24() real ext-real set
b is ext-real Element of ExtREAL
a is V24() real ext-real set
b is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
(-infty,+infty) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not +infty <= b₁ ) } is set
1 is non empty natural V24() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
[.0,1.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
[.0,+infty.[ is complex-membered ext-real-membered real-membered non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( 0 <= b₁ & not +infty <= b₁ ) } is set
-infty is non empty non real ext-real non positive negative Element of ExtREAL
1 is non empty natural V24() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
].-infty,1.] is complex-membered ext-real-membered real-membered non left_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= 1 ) } is set
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
(a,b) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= a & not b <= b₁ ) } is set
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
a is V24() real ext-real set
b is V24() real ext-real set
[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & b₁ <= b ) } is set
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
a is V24() real ext-real set
b is ext-real Element of ExtREAL
[.a,b.[ is complex-membered ext-real-membered real-membered non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & not b <= b₁ ) } is set
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
a is ext-real Element of ExtREAL
b is V24() real ext-real set
].a,b.] is complex-membered ext-real-membered real-membered non left_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= a & b₁ <= b ) } is set
X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf X is ext-real Element of ExtREAL
sup X is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
[.a,b.] is ext-real-membered interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & b₁ <= b ) } is set
inf X is ext-real Element of ExtREAL
sup X is ext-real Element of ExtREAL
].(inf X),(sup X).] is ext-real-membered non left_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= inf X & b₁ <= sup X ) } is set
inf X is ext-real Element of ExtREAL
sup X is ext-real Element of ExtREAL
[.(inf X),(sup X).[ is ext-real-membered non right_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( inf X <= b₁ & not sup X <= b₁ ) } is set
a is ext-real set
b is ext-real set
].a,b.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= a & not b <= b₁ ) } is set
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
{-infty,+infty} is non empty V36() ext-real-membered left_end right_end set
b is V24() real ext-real Element of REAL
a is V24() real ext-real Element of REAL
b is V24() real ext-real set
c₆ is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
b is V24() real ext-real Element of REAL
a is V24() real ext-real set
b is V24() real ext-real Element of REAL
c₆ is ext-real Element of ExtREAL
b is V24() real ext-real Element of REAL
a is V24() real ext-real set
b is V24() real ext-real Element of REAL
c₆ is ext-real Element of ExtREAL
0. is empty ext-real non positive non negative V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval Element of ExtREAL
a is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
min (a,b) is ext-real set
{a,b} is non empty V36() ext-real-membered left_end right_end set
inf {a,b} is ext-real set
a is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
c₆ is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
max (X,a) is ext-real set
{X,a} is non empty V36() ext-real-membered left_end right_end set
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
sup {X,a} is ext-real set
X is ext-real-membered set
sup X is ext-real Element of ExtREAL
inf X is ext-real Element of ExtREAL
(sup X) - (inf X) is ext-real Element of ExtREAL
K166((inf X)) is ext-real set
K165((sup X),K166((inf X))) is ext-real set
0. is empty ext-real non positive non negative V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval Element of ExtREAL
a is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
(X,a) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= X & not a <= b₁ ) } is set
((X,a)) is ext-real Element of ExtREAL
a - X is ext-real Element of ExtREAL
K166(X) is ext-real set
K165(a,K166(X)) is ext-real set
sup (X,a) is ext-real Element of ExtREAL
inf (X,a) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
[.X,a.] is ext-real-membered interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( X <= b₁ & b₁ <= a ) } is set
([.X,a.]) is ext-real Element of ExtREAL
a - X is ext-real Element of ExtREAL
K166(X) is ext-real set
K165(a,K166(X)) is ext-real set
sup [.X,a.] is ext-real Element of ExtREAL
inf [.X,a.] is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
[.X,a.[ is ext-real-membered non right_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( X <= b₁ & not a <= b₁ ) } is set
([.X,a.[) is ext-real Element of ExtREAL
a - X is ext-real Element of ExtREAL
K166(X) is ext-real set
K165(a,K166(X)) is ext-real set
sup [.X,a.[ is ext-real Element of ExtREAL
inf [.X,a.[ is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
].X,a.] is ext-real-membered non left_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= X & b₁ <= a ) } is set
(].X,a.]) is ext-real Element of ExtREAL
a - X is ext-real Element of ExtREAL
K166(X) is ext-real set
K165(a,K166(X)) is ext-real set
sup ].X,a.] is ext-real Element of ExtREAL
inf ].X,a.] is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(X) is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
b is ext-real Element of ExtREAL
(a,b) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= a & not b <= b₁ ) } is set
[.a,b.] is ext-real-membered interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & b₁ <= b ) } is set
[.a,b.[ is ext-real-membered non right_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & not b <= b₁ ) } is set
].a,b.] is ext-real-membered non left_end interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= a & b₁ <= b ) } is set
sup X is ext-real Element of ExtREAL
inf X is ext-real Element of ExtREAL
b - a is ext-real Element of ExtREAL
K166(a) is ext-real set
K165(b,K166(a)) is ext-real set
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
(0.,0.) is empty proper V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= 0. & not 0. <= b₁ ) } is set
({}) is ext-real Element of ExtREAL
X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(X) is ext-real Element of ExtREAL
inf X is ext-real Element of ExtREAL
sup X is ext-real Element of ExtREAL
(sup X) - (inf X) is ext-real Element of ExtREAL
K166((inf X)) is ext-real set
K165((sup X),K166((inf X))) is ext-real set
X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(X) is ext-real Element of ExtREAL
a is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(a) is ext-real Element of ExtREAL
sup a is ext-real Element of ExtREAL
inf a is ext-real Element of ExtREAL
(sup a) - (inf a) is ext-real Element of ExtREAL
K166((inf a)) is ext-real set
K165((sup a),K166((inf a))) is ext-real set
sup X is ext-real Element of ExtREAL
inf X is ext-real Element of ExtREAL
(sup X) - (inf X) is ext-real Element of ExtREAL
K166((inf X)) is ext-real set
K165((sup X),K166((inf X))) is ext-real set
X is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
[.X,a.] is ext-real-membered interval set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( X <= b₁ & b₁ <= a ) } is set
b is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(b) is ext-real Element of ExtREAL
a is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(a) is ext-real Element of ExtREAL
{X} is non empty V36() ext-real-membered left_end right_end set
inf a is ext-real Element of ExtREAL
sup a is ext-real Element of ExtREAL
X - X is ext-real Element of ExtREAL
K166(X) is ext-real set
K165(X,K166(X)) is ext-real set
X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
a is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(X) is ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL
X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
(X) is ext-real Element of ExtREAL
X is complex-membered ext-real-membered real-membered Element of K32(REAL)
a is V24() real ext-real set
b is V24() real ext-real set
[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & b₁ <= b ) } is set
a is V24() real ext-real Element of REAL
b is V24() real ext-real Element of REAL
[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & b₁ <= b ) } is set
a is V24() real ext-real Element of REAL
b is V24() real ext-real Element of REAL
[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
{ b₁ where b₁ is ext-real Element of ExtREAL : ( a <= b₁ & b₁ <= b ) } is set