denselyOrdered_range_norm — Mathlib

English

The set range of the norm is densely ordered: between any two norms there exists a third norm value.

Русский

Область значений нормы плотно упорядочена: между двумя значениями найдётся третье.

LaTeX

$$$ \text{DenselyOrdered} (\mathrm{Set.range} (\mathrm{norm} : α \to \mathbb{R})) $$$

Lean4

instance denselyOrdered_range_norm : DenselyOrdered (Set.range (norm : α → ℝ)) where
  dense := by
    rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
    let ⟨z, h⟩ := exists_lt_norm_lt α (norm_nonneg _) hxy
    exact ⟨⟨‖z‖, z, rfl⟩, h⟩

Похожие утверждения