norm_smul_eq — Mathlib

English

On the same ray, the norms satisfy a proportional equality: ||x|| y = ||y|| x.

Русский

На одном луче величины нормы удовлетворяют пропорциональному равенству: ||x|| y = ||y|| x.

LaTeX

$$$$ \forall \text{SameRay}(\mathbb{R},x,y)\; \|x\| \cdot y = \|y\| \cdot x. $$$$

Lean4

theorem norm_smul_eq (h : SameRay ℝ x y) : ‖x‖ • y = ‖y‖ • x :=
  by
  rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
  simp only [norm_smul_of_nonneg, *, mul_smul]
  rw [smul_comm, smul_comm b, smul_comm a b u]

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