exists_norm_eq — Mathlib

English

Let E be a nontrivial real normed space. For every nonnegative real c, there exists x ∈ E such that ‖x‖ = c.

Русский

Пусть E — ненулевое вещественное нормированное пространство. Для каждого неотрицательного числа c найдется вектор x ∈ E such that ‖x‖ = c.

LaTeX

$$$$ \forall c \in \mathbb{R}, \ c \ge 0 \Rightarrow \exists x \in E \; \|x\| = c. $$$$

Lean4

theorem exists_norm_eq {c : ℝ} (hc : 0 ≤ c) : ∃ x : E, ‖x‖ = c :=
  by
  rcases exists_ne (0 : E) with ⟨x, hx⟩
  rw [← norm_ne_zero_iff] at hx
  use c • ‖x‖⁻¹ • x
  simp [norm_smul, Real.norm_of_nonneg hc, inv_mul_cancel₀ hx]

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