exists_lt_norm_lt — Mathlib

English

In a densely normed field, for r1 ≤ r2 with r1 < r2, there exists x with r1 < ∥x∥ and ∥x∥ < r2.

Русский

В плоскости плотно нормированного поля, при r1 ≤ r2 и r1 < r2 существует x с r1 < ∥x∥ < r2.

LaTeX

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

Lean4

theorem exists_lt_norm_lt {r₁ r₂ : ℝ} (h₀ : 0 ≤ r₁) (h : r₁ < r₂) : ∃ x : α, r₁ < ‖x‖ ∧ ‖x‖ < r₂ :=
  DenselyNormedField.lt_norm_lt r₁ r₂ h₀ h

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