normalize_smul_of_pos — Mathlib

English

If r > 0, then normalization is homogeneous of degree 0: normalize(r x) = normalize(x).

Русский

Если r > 0, то нормирование не изменяет направление: normalize(r x) = normalize(x).

LaTeX

$$$0 < r \\implies \\operatorname{normalize}(r \\cdot x) = \\operatorname{normalize}(x)$$$

Lean4

theorem normalize_smul_of_pos {r : ℝ} (hr : 0 < r) (x : V) : normalize (r • x) = normalize x := by
  simp [normalize, norm_smul, smul_smul, abs_of_pos hr, hr.ne']

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