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
Real interval
Definition D2424
Set of real intervals
Formulation 0
Let $\mathcal{P}_{\text{open}} = \mathcal{P}_{\text{open}}(\mathbb{R})$ be the D2615: Set of open real intervals.
Let $\mathcal{P}_{\text{closed}} = \mathcal{P}_{\text{closed}}(\mathbb{R})$ be the D2425: Set of closed real intervals.
Let $\mathcal{P}_{\text{right-closed}} = \mathcal{P}_{\text{right-closed}}(\mathbb{R})$ be the D3004: Set of right-closed real intervals.
Let $\mathcal{P}_{\text{left-closed}} = \mathcal{P}_{\text{left-closed}}(\mathbb{R})$ be the D3005: Set of left-closed real intervals.
The set of real intervals is the D11: Set \begin{equation} \mathcal{P}_{\text{open}} \cup \mathcal{P}_{\text{closed}} \cup \mathcal{P}_{\text{right-closed}} \cup \mathcal{P}_{\text{left-closed}} \end{equation}
Results
R2970: The four classes of real intervals are each closed under translation