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]