abs_oangle_sub_right_toReal_lt_pi_div_two

English

Under the same hypotheses as before, the real angle between y−x and y is acute in the sense that its absolute value is less than π/2.

Русский

При тех же предположениях абсолютное значение угла между y−x и y меньше π/2.

LaTeX

$$$\\forall x,y\\in V,\\ \\|x\\| = \\|y\\| \\Rightarrow |(o.oangle(y - x)\\,y).toReal| < \\frac{\\pi}{2}$$$

Lean4

/-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/
theorem abs_oangle_sub_right_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) : |(o.oangle x (x - y)).toReal| < π / 2 :=
  (o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h).symm ▸ o.abs_oangle_sub_left_toReal_lt_pi_div_two h

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