denselyOrdered_range_nnnorm — Mathlib

English

The set range of the NNNorm (nnnorm) is densely ordered.

Русский

Диапазон значений nnNorm плотно упорядочен.

LaTeX

$$$ \text{DenselyOrdered} (\mathrm{Set.range} \big( \mathrm{nnnorm} : α \to \mathbb{R}_{\ge 0} \)) $$$

Lean4

instance denselyOrdered_range_nnnorm : DenselyOrdered (Set.range (nnnorm : α → ℝ≥0)) where
  dense := by
    rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
    let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
    exact ⟨⟨‖z‖₊, z, rfl⟩, h⟩

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