Extended Real Line (拡張実数直線) (Example I.3.9)
- Extended Real Line (拡張実数直線) (Example I.3.9) #Card
- $(\overline{\mathbb{R}}, \leq)$ with $\overline{\mathbb{R}} := \mathbb{R} \cup {-\infty, +\infty}$ is a complete lattice, while $(\mathbb{R}, \leq)$ is only a relatively complete lattice.
The ordered extended real line $(\overline{\mathbb{R}}, \leq)$, where $\overline{\mathbb{R}} := \mathbb{R} \cup {-\infty, +\infty}$, is a complete lattice（すべての空でない部分集合が sup・inf を持つ）, while the ordered real line $(\mathbb{R}, \leq)$ is only a relatively complete lattice: 空でない有界集合だけが sup（上に有界のとき）・inf（下に有界のとき）を持つ。
- $\mathbb{Q}$ では相対完備性も失敗する: ${q \in \mathbb{Q} : q^2 < 2}$ は上に有界だが sup を持たない（$\sqrt 2 \notin \mathbb{Q}$）。
- 測度論・積分論で $\overline{\mathbb{R}}$（
ℝ≥0∞含む）が既定の値域になる理由——sup/inf が常に取れる。
EReal（CompleteLinearOrder）；非負版は ℝ≥0∞ (ENNReal)。$\mathbb{R}$ の相対完備性は Real.instConditionallyCompleteLinearOrder