exists_lt_nnnorm_lt — Mathlib

English

In a densely normed field, for r1 < r2 with r1, r2 in NNReal, there exists x with r1 < ‖x‖₊ and ‖x‖₊ < r2.

Русский

В плотно нормированном поле для NNReal r1 < r2 существует x с r1 < ‖x‖₊ и ‖x‖₊ < r2.

LaTeX

$$$ \exists x : α, r_1 < \|x\|_+ \land \|x\|_+ < r_2 $$$

Lean4

theorem exists_lt_nnnorm_lt {r₁ r₂ : ℝ≥0} (h : r₁ < r₂) : ∃ x : α, r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂ :=
  mod_cast exists_lt_norm_lt α r₁.prop h

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