norm_smul_inv_norm' — Mathlib

English

Let r≥0 be a real, x ≠ 0 in a normed space over 𝕜. Then ‖(‖x‖)^{-1} • x‖ = 1, up to the appropriate 𝕜-scalar interpretation.

Русский

Пусть r ≥ 0 и x ≠ 0 в нормированном пространстве над 𝕜. Тогда ‖(‖x‖)^{-1} • x‖ = 1 с учетом соответствующего поля 𝕜.

LaTeX

$$$\\| (\\|x\\|^{-1} : \\mathbb{K}) \\cdot x \\| = 1$$$

Lean4

/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to length `r`. -/
theorem norm_smul_inv_norm' {r : ℝ} (r_nonneg : 0 ≤ r) {x : E} (hx : x ≠ 0) : ‖((r : 𝕜) * (‖x‖ : 𝕜)⁻¹) • x‖ = r :=
  by
  have : ‖x‖ ≠ 0 := by simp [hx]
  simp [field, norm_smul, r_nonneg, rclike_simps]

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