denselyNormedField

Mathlib.Analysis.Normed.Field.Basic

URI: https://scilib.ai/kg/mathlib#Real.denselyNormedField

← MathLib Explorer

English

Real numbers carry a densely normed field structure.

Русский

Набор действительных чисел обладает плотной нормировкой.

LaTeX

$$$ \mathbb{R} ext{ is densely normed field} $$$

Lean4

noncomputable instance denselyNormedField : DenselyNormedField ℝ where
  lt_norm_lt _ _ h₀
    hr :=
    let ⟨x, h⟩ := exists_between hr
    ⟨x, by rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru