:: XXREAL_2 semantic presentation

REAL is complex-membered ext-real-membered real-membered V10() non empty V13() non finite set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() V13() non finite Element of K12(REAL)
K12(REAL) is V13() non finite cup-closed diff-closed preBoolean set
+infty is ext-real positive non negative non real non empty set
-infty is ext-real non positive negative non real non empty set
0 is ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() real empty ordinal natural integer finite V37() rational V51() Element of NAT
[0,REAL] is set
{0,REAL} is non empty finite set
{0} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V37() set
{{0,REAL},{0}} is non empty finite V37() set
ExtREAL is ext-real-membered non empty set
{+infty,-infty} is ext-real-membered non empty finite set
REAL \/ {+infty,-infty} is ext-real-membered non empty set
{} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() empty finite V37() set
].-infty,+infty.[ is complex-membered ext-real-membered real-membered set
1 is ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real non empty ordinal natural integer finite rational V51() Element of NAT
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V10() non empty V13() non finite set
F₁() is ext-real real integer V51() set
F₂() is ext-real real integer V51() set
{ F₃(b₁) where b₁ is ext-real real integer rational V51() Element of INT : ( F₁() <= b₁ & b₁ <= F₂() & P₁[b₁] ) } is set
B is set
s1 is ext-real real integer rational V51() Element of INT
F₃(s1) is set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() empty finite V37() set
F₂() - F₁() is ext-real real integer V51() set
B is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real ordinal natural integer finite rational V51() Element of NAT
B + 1 is ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real non empty ordinal natural integer finite rational V51() Element of NAT
x is set
y is ext-real non negative real ordinal natural integer finite V51() set
y + F₁() is ext-real real integer V51() set
F₃((y + F₁())) is set
x is Relation-like Function-like set
dom x is set
rng x is set
y is set
r is ext-real real integer rational V51() Element of INT
F₃(r) is set
r - F₁() is ext-real real integer V51() set
l is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real ordinal natural integer finite rational V51() Element of NAT
x . (r - F₁()) is set
r + F₁() is ext-real real integer V51() set
(r + F₁()) - F₁() is ext-real real integer V51() set
F₃(((r + F₁()) - F₁())) is set
c₈ is ext-real real integer V51() set
c₈ + F₁() is ext-real real integer V51() set
F₃((c₈ + F₁())) is set
A is ext-real-membered set
B is ext-real set
B is ext-real set
A is ext-real-membered set
B is ext-real set
s1 is ext-real set
B is ext-real set
s1 is ext-real (A)
B is ext-real set
s1 is ext-real set
B is ext-real set
s1 is ext-real set
B is ext-real set
s1 is ext-real (A)
B is ext-real set
s1 is ext-real set
A is ext-real set
B is ext-real set
{B} is ext-real-membered non empty finite set
s1 is ext-real set
A is ext-real set
B is ext-real set
{B} is ext-real-membered non empty finite set
s1 is ext-real set
A is ext-real set
{A} is ext-real-membered non empty finite set
({A}) is ext-real set
B is ext-real ({A})
A is ext-real set
{A} is ext-real-membered non empty finite set
({A}) is ext-real set
B is ext-real ({A})
Fin ExtREAL is non empty cup-closed diff-closed preBoolean set
A is finite Element of Fin ExtREAL
A is ext-real set
B is ext-real-membered set
(B) is ext-real set
A is ext-real set
B is ext-real-membered set
(B) is ext-real set
A is ext-real-membered set
B is ext-real-membered set
s1 is ext-real (B)
x is ext-real set
A is ext-real-membered set
B is ext-real-membered set
s1 is ext-real (B)
x is ext-real set
A is ext-real-membered set
B is ext-real-membered set
A \/ B is ext-real-membered set
s1 is ext-real (A)
x is ext-real (B)
min (s1,x) is ext-real set
r is ext-real set
A is ext-real-membered set
B is ext-real-membered set
A \/ B is ext-real-membered set
s1 is ext-real (A)
x is ext-real (B)
max (s1,x) is ext-real set
r is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real-membered set
A \/ B is ext-real-membered set
((A \/ B)) is ext-real set
(B) is ext-real set
min ((A),(B)) is ext-real set
x is ext-real (A \/ B)
A is ext-real-membered set
(A) is ext-real set
B is ext-real-membered set
A \/ B is ext-real-membered set
((A \/ B)) is ext-real set
(B) is ext-real set
max ((A),(B)) is ext-real set
x is ext-real (A \/ B)
A is ext-real-membered non empty set
B is ext-real-membered non empty finite Element of Fin ExtREAL
s1 is ext-real-membered non empty finite Element of Fin ExtREAL
B \/ s1 is ext-real-membered non empty finite Element of Fin ExtREAL
((B \/ s1)) is ext-real set
(B) is ext-real set
(s1) is ext-real set
min ((B),(s1)) is ext-real set
((B \/ s1)) is ext-real set
(B) is ext-real set
(s1) is ext-real set
max ((B),(s1)) is ext-real set
B is ext-real Element of ExtREAL
{.B.} is ext-real-membered non empty finite Element of Fin ExtREAL
{B} is ext-real-membered non empty finite set
({B}) is ext-real set
({B}) is ext-real set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty set
B is ext-real non negative real ordinal natural integer finite V51() set
s1 is ext-real set
s1 is ext-real (A)
(A) is ext-real set
A is ext-real-membered () set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
s1 is ext-real (A)
A is ext-real-membered () set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
s1 is ext-real (A)
A is ext-real set
{A} is ext-real-membered non empty finite () () set
({A}) is ext-real set
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
s1 is ext-real set
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
s1 is ext-real ({A,B})
A is ext-real set
B is ext-real set
max (A,B) is ext-real set
{A,B} is ext-real-membered non empty finite () () set
({A,B}) is ext-real set
s1 is ext-real ({A,B})
s1 is ext-real ({A,B})
A is ext-real set
{A} is ext-real-membered non empty finite () () set
({A}) is ext-real set
A is ext-real set
B is ext-real set
{B,A} is ext-real-membered non empty finite () () set
s1 is ext-real set
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
s1 is ext-real ({A,B})
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
({A,B}) is ext-real set
min (A,B) is ext-real set
s1 is ext-real ({A,B})
s1 is ext-real ({A,B})
A is ext-real-membered set
A is ext-real-membered set
A is complex-membered ext-real-membered real-membered set
B is ext-real set
B is ext-real set
B is complex-membered ext-real-membered real-membered non empty finite () () set
(B) is ext-real set
(A) is ext-real set
s1 is ext-real real V51() set
x is ext-real set
(B) is ext-real set
(A) is ext-real set
x is ext-real real V51() set
y is ext-real set
A is complex-membered ext-real-membered real-membered non empty set
(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() set
A is complex-membered ext-real-membered real-membered non empty set
(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() set
A is complex-membered ext-real-membered real-membered non empty () set
(A) is ext-real set
A is complex-membered ext-real-membered real-membered non empty () set
(A) is ext-real set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty () set
(B) is ext-real real V51() set
[\(B)/] is ext-real real integer V51() set
x is ext-real set
(A) is ext-real set
x is ext-real real integer V51() set
x - 1 is ext-real real integer V51() set
y is ext-real set
r is ext-real real integer V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty () set
(B) is ext-real real V51() set
[/(B)\] is ext-real real integer V51() set
x is ext-real set
(A) is ext-real set
x is ext-real real integer V51() set
x + 1 is ext-real real integer V51() set
y is ext-real set
r is ext-real real integer V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
B is ext-real set
A is complex-membered ext-real-membered real-membered () set
(A) is ext-real set
A is complex-membered ext-real-membered real-membered rational-membered () set
(A) is ext-real real V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered () set
(A) is ext-real real rational V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered () () set
(A) is ext-real real integer rational V51() set
A is complex-membered ext-real-membered real-membered () set
(A) is ext-real set
A is complex-membered ext-real-membered real-membered rational-membered () set
(A) is ext-real real V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered () set
(A) is ext-real real rational V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered () () set
(A) is ext-real real integer rational V51() set
A is complex-membered ext-real-membered real-membered set
(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real set
A is complex-membered ext-real-membered real-membered set
(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real set
A is ext-real set
B is ext-real set
[.A,B.] is ext-real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
].A,B.] is ext-real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
[.A,B.[ is ext-real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
].A,B.[ is complex-membered ext-real-membered real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
[.B,A.] is ext-real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
].B,A.] is ext-real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
[.B,A.[ is ext-real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
].B,A.[ is complex-membered ext-real-membered real-membered set
s1 is ext-real set
A is ext-real set
B is ext-real set
[.A,B.] is ext-real-membered set
([.A,B.]) is ext-real set
s1 is ext-real ([.A,B.])
A is ext-real set
B is ext-real set
[.A,B.[ is ext-real-membered set
([.A,B.[) is ext-real set
s1 is ext-real ([.A,B.[)
A is ext-real set
B is ext-real set
].A,B.] is ext-real-membered set
(].A,B.]) is ext-real set
s1 is ext-real (].A,B.])
x is ext-real set
A is ext-real set
B is ext-real set
].A,B.[ is complex-membered ext-real-membered real-membered set
(].A,B.[) is ext-real set
s1 is ext-real (].A,B.[)
x is ext-real set
A is ext-real set
B is ext-real set
[.A,B.] is ext-real-membered set
([.A,B.]) is ext-real set
s1 is ext-real ([.A,B.])
A is ext-real set
B is ext-real set
].A,B.] is ext-real-membered set
(].A,B.]) is ext-real set
s1 is ext-real (].A,B.])
A is ext-real set
B is ext-real set
[.A,B.[ is ext-real-membered set
([.A,B.[) is ext-real set
s1 is ext-real ([.A,B.[)
x is ext-real set
A is ext-real set
B is ext-real set
].A,B.[ is complex-membered ext-real-membered real-membered set
(].A,B.[) is ext-real set
s1 is ext-real (].A,B.[)
x is ext-real set
A is ext-real set
B is ext-real set
[.A,B.] is ext-real-membered set
([.A,B.]) is ext-real set
([.A,B.]) is ext-real set
A is ext-real set
B is ext-real set
[.A,B.[ is ext-real-membered set
([.A,B.[) is ext-real set
A is ext-real set
B is ext-real set
].A,B.] is ext-real-membered set
(].A,B.]) is ext-real set
A is ext-real set
B is ext-real set
A is ext-real set
B is ext-real set
({}) is ext-real set
A is ext-real ( {} )
({}) is ext-real set
A is ext-real ( {} )
A is ext-real-membered set
(A) is ext-real set
(A) is ext-real set
B is ext-real set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty () () () () () set
(B) is ext-real real integer rational V51() set
(B) is ext-real real integer rational V51() set
{ H₁(b₁) where b₁ is ext-real real integer rational V51() Element of INT : ( (B) <= b₁ & b₁ <= (B) & S₁[b₁] ) } is set
r is ext-real real integer V51() set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite () () () set
A is ext-real-membered set
B is ext-real set
A is ext-real-membered set
B is ext-real set
A is ext-real-membered set
B is ext-real-membered set
s1 is ext-real real V51() set
A is ext-real-membered set
B is ext-real-membered set
s1 is ext-real real V51() set
A is ext-real-membered set
B is ext-real-membered set
A is ext-real real V51() set
B is ext-real real V51() set
A is ext-real real V51() set
B is ext-real real V51() set
{+infty} is ext-real-membered non empty finite () () set
A is ext-real set
{-infty} is ext-real-membered non empty finite () () set
A is ext-real set
A is ext-real-membered non empty () set
B is set
x is ext-real real V51() set
s1 is ext-real set
A is ext-real-membered non empty () set
B is set
x is ext-real real V51() set
s1 is ext-real set
A is ext-real-membered set
B is ext-real set
A is ext-real-membered set
B is ext-real set
A is ext-real-membered non empty set
B is ext-real (A)
s1 is ext-real set
s1 is ext-real real V51() set
A is ext-real-membered non empty set
B is ext-real (A)
s1 is ext-real set
s1 is ext-real real V51() set
A is ext-real-membered non empty set
(A) is ext-real set
B is ext-real (A)
s1 is ext-real (A)
A is ext-real-membered non empty set
(A) is ext-real set
B is ext-real (A)
s1 is ext-real (A)
A is ext-real-membered non empty set
(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() Element of REAL
A is ext-real-membered non empty set
(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() Element of REAL
A is ext-real-membered set
B is ext-real-membered set
(A) is ext-real set
(B) is ext-real set
A is ext-real-membered set
B is ext-real-membered set
(B) is ext-real set
(A) is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
A is ext-real-membered set
B is ext-real-membered set
(A) is ext-real set
(B) is ext-real set
s1 is ext-real set
x is ext-real set
B is ext-real-membered set
A is ext-real-membered set
(A) is ext-real set
(B) is ext-real set
s1 is ext-real set
x is ext-real set
A is ext-real-membered set
B is ext-real-membered set
A /\ B is ext-real-membered set
s1 is ext-real (A)
x is ext-real (B)
min (s1,x) is ext-real set
y is ext-real set
A is ext-real-membered set
B is ext-real-membered set
A /\ B is ext-real-membered set
s1 is ext-real (A)
x is ext-real (B)
max (s1,x) is ext-real set
y is ext-real set
A is ext-real-membered set
B is ext-real-membered set
A /\ B is ext-real-membered set
((A /\ B)) is ext-real set
(A) is ext-real set
(B) is ext-real set
min ((A),(B)) is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real-membered set
(B) is ext-real set
max ((A),(B)) is ext-real set
A /\ B is ext-real-membered set
((A /\ B)) is ext-real set
A is ext-real-membered set
B is set
s1 is ext-real-membered non empty set
x is ext-real real V51() set
y is ext-real set
r is ext-real real V51() set
A is ext-real-membered set
(A) is ext-real set
(A) is ext-real set
[.(A),(A).] is ext-real-membered set
B is ext-real set
A is ext-real-membered set
(A) is ext-real set
(A) is ext-real set
{(A)} is ext-real-membered non empty finite () () set
[.(A),(A).] is ext-real-membered non empty set
A is ext-real set
B is ext-real set
s1 is ext-real-membered set
x is ext-real set
A is ext-real set
B is ext-real set
s1 is ext-real-membered set
x is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real real V51() set
A is ext-real-membered set
(A) is ext-real set
B is ext-real real V51() set
A is ext-real set
B is ext-real set
[.A,B.] is ext-real-membered set
A is ext-real-membered set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered set
A is ext-real set
B is ext-real set
[.A,B.] is ext-real-membered set
s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered set
y is ext-real set
].A,B.] is ext-real-membered set
s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
y is ext-real set
[.A,B.[ is ext-real-membered set
s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
y is ext-real set
].A,B.[ is complex-membered ext-real-membered real-membered set
s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
y is ext-real set
A is ext-real-membered () set
B is ext-real-membered () set
A /\ B is ext-real-membered set
s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
A is ext-real set
B is ext-real set
].A,B.] is ext-real-membered () set
(].A,B.]) is ext-real set
[.A,B.[ is ext-real-membered () set
([.A,B.[) is ext-real set
].A,B.[ is complex-membered ext-real-membered real-membered () set
(].A,B.[) is ext-real set
(].A,B.[) is ext-real set
[.0,1.] is complex-membered ext-real-membered real-membered () set
].0,1.] is complex-membered ext-real-membered real-membered () () set
[.0,1.[ is complex-membered ext-real-membered real-membered () () set
2 is ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real non empty ordinal natural integer finite rational V51() () () () () () Element of NAT
].0,2.[ is complex-membered ext-real-membered real-membered () () () set
A is ext-real-membered () () () set
(A) is ext-real set
(A) is ext-real set
[.(A),(A).] is ext-real-membered () set
B is ext-real set
A is ext-real-membered () () () set
(A) is ext-real set
(A) is ext-real set
].(A),(A).] is ext-real-membered () () set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
[.s1,(A).] is ext-real-membered () set
s1 is ext-real set
A is ext-real-membered () () () set
(A) is ext-real set
(A) is ext-real set
[.(A),(A).[ is ext-real-membered () () set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
[.(A),s1.] is ext-real-membered () set
s1 is ext-real set
A is ext-real-membered non empty () () () set
(A) is ext-real set
(A) is ext-real set
].(A),(A).[ is complex-membered ext-real-membered real-membered () () () set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
x is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
s1 is ext-real set
x is ext-real set
A is ext-real-membered () () () set
].-infty,-infty.[ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() empty finite V37() () () () () () () set
(A) is ext-real set
(A) is ext-real set
].(A),(A).[ is complex-membered ext-real-membered real-membered () () () set
A is ext-real-membered set
B is ext-real set
s1 is ext-real set
x is ext-real set
[.B,s1.] is ext-real-membered () set
A is ext-real-membered set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
x is ext-real set
x is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
x is ext-real set
x is ext-real set
A is ext-real-membered set
(A) is ext-real set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
A is ext-real-membered set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set
A is ext-real-membered set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set
A is ext-real-membered set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set
A is ext-real-membered set
(A) is ext-real set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set
A is ext-real-membered set
B is ext-real set
s1 is ext-real set
x is ext-real set
A is ext-real-membered set
B is ext-real-membered set
A \/ B is ext-real-membered set
s1 is ext-real set
x is ext-real set
y is ext-real set
r is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real-membered set
(B) is ext-real set
A \/ B is ext-real-membered set
x is ext-real set
y is ext-real set
r is ext-real set
A is ext-real-membered set
(A) is ext-real set
B is ext-real-membered set
(B) is ext-real set
A \/ B is ext-real-membered set
x is ext-real set
y is ext-real set
r is ext-real set
A is ext-real-membered set
(A) is ext-real set
A is ext-real-membered set
(A) is ext-real set
K12(ExtREAL) is cup-closed diff-closed preBoolean set
A is ext-real-membered non empty Element of K12(ExtREAL)
B is ext-real Element of A
A is ext-real-membered non empty Element of K12(ExtREAL)
B is ext-real Element of A
A is ext-real-membered non empty Element of K12(ExtREAL)
(A) is ext-real set
B is ext-real set
s1 is ext-real set
A is ext-real-membered non empty Element of K12(ExtREAL)
(A) is ext-real set
B is ext-real Element of ExtREAL
s1 is ext-real set
A is ext-real-membered non empty Element of K12(ExtREAL)
B is ext-real-membered non empty Element of K12(ExtREAL)
(A) is ext-real set
(B) is ext-real set
s1 is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL