ThmDex – An index of mathematical definitions, results, and 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
Interval
Set of intervals
J-interval
N-interval
Real N-interval
Set of euclidean real intervals
Definition D3757
Elementary euclidean real set
Formulation 0
Let $\mathbb{R}^N$ be a D5630: Set of euclidean real numbers such that
(i) $\mathcal{P}_{\text{interval}}(\mathbb{R}^N)$ is the D3037: Set of euclidean real intervals in $\mathbb{R}^N$
A D11: Set $E \subseteq \mathbb{R}^N$ is an elementary euclidean real set in $\mathbb{R}^N$ if and only if \begin{equation} \exists \, I_1, \ldots, I_N \in \mathcal{P}_{\text{interval}}(\mathbb{R}) : E = \bigcup_{n = 1}^N I_n \end{equation}