instDenselyNormedField — Mathlib

English

The complex numbers form a densely normed field; i.e., between any two real numbers there are complex elements, and the field is normed.

Русский

Комплексные числа образуют плотно нормированное поле; между любыми двумя действительными числами есть комплексные элементы, и поле нормировано.

LaTeX

$$$ \\text{DenselyNormedField } \\mathbb{C}$$$

Lean4

instance : DenselyNormedField ℂ where
  lt_norm_lt r₁ r₂ h₀
    hr :=
    let ⟨x, h⟩ := exists_between hr
    ⟨x, by rwa [norm_real, Real.norm_of_nonneg (h₀.trans_lt h.1).le]⟩

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