Loading [MathJax]/jax/output/CommonHTML/jax.js
ThmDex – An index of mathematical definitions, results, and conjectures.
Definitions
,
Results
,
Conjectures
▼
Set of symbols
▼
Alphabet
▼
Deduction system
▼
Theory
▼
Zermelo-Fraenkel set theory
▼
Set
▼
Binary cartesian set product
▼
Binary relation
▼
Binary endorelation
▼
Preordering relation
▼
Partial ordering relation
▼
Partially ordered set
▼
Closed interval
Definition D544
Closed real interval
Formulation 0
Let
P
=
(
R
,
≤
)
be the
D1102: Ordered set of real numbers
such that
(i)
a
,
b
∈
R
are each a
D993: Real number
The
closed real interval
from
a
to
b
is the
D11: Set
[
a
,
b
]
:=
{
x
∈
R
:
a
≤
x
≤
b
}
Formulation 1
Let
P
=
(
R
,
≤
)
be the
D1102: Ordered set of real numbers
such that
(i)
a
,
b
∈
R
are each a
D993: Real number
The
closed real interval
from
a
to
b
is the
D11: Set
[
a
,
b
]
:=
{
x
∈
R
:
a
≤
x
,
x
≤
b
}
Children
▶
D1510: Closed real unit interval
▶
D543: Open real interval