oangle_smul_smul_self_of_nonneg — Mathlib

English

The angle between two nonnegative multiples of the same vector is 0: o.oangle(r1·x, r2·x) = 0 for r1,r2 ≥ 0.

Русский

Угол между двумя ненегативными кратными одним и тем же вектору равен 0: o.oangle(r1·x, r2·x) = 0 при r1,r2 ≥ 0.

LaTeX

$$$r_1 \ge 0, r_2 \ge 0 \Rightarrow o.oangle\;(r_1\cdot x)\;(r_2\cdot x) = 0$$$

Lean4

/-- The angle between two nonnegative multiples of the same vector is 0. -/
@[simp]
theorem oangle_smul_smul_self_of_nonneg (x : V) {r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hr₂ : 0 ≤ r₂) :
    o.oangle (r₁ • x) (r₂ • x) = 0 := by
  rcases hr₁.lt_or_eq with (h | h)
  · simp [h, hr₂]
  · simp [h.symm]

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