inv_norm_smul_mem_unitClosedBall — Mathlib

English

For any x in a normed space, the vector x scaled by its reciprocal norm lies in the unit closed ball.

Русский

Любой вектор x в нормированном пространстве, умноженный на обратную норму, лежит в замкнутой единичной окрестности.

LaTeX

$$$\\|x\\|^{-1} \\cdot x \\in \\overline{B}(0,1)$$$

Lean4

theorem inv_norm_smul_mem_unitClosedBall (x : E) : ‖x‖⁻¹ • x ∈ closedBall (0 : E) 1 := by
  simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul, div_self_le_one]

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