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

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 $$\mathcal{P}_{\text{open}} \cup \mathcal{P}_{\text{closed}} \cup \mathcal{P}_{\text{right-closed}} \cup \mathcal{P}_{\text{left-closed}}$$
Results
 ▶ The four classes of real intervals are each closed under translation