abs_oangle_center_left_toReal_lt_pi_div_two

English

The center can also be written using the reciprocal of tan of the angle and the π/2 rotation, plus the midpoint.

Русский

Центр выражается через обратное кtan угла и вращение на π/2, плюс середина.

LaTeX

$$$((\\tan(\\angle p_1 p_2 p_3))^{-1}/2) \\cdot o.rotation_{\\pi/2}(p_3 - p_1) + midpoint(p_1,p_3) = s.center$$$

Lean4

/-- A base angle of an isosceles triangle with apex at the center of a circle is acute. -/
theorem abs_oangle_center_left_toReal_lt_pi_div_two {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    |(∡ s.center p₂ p₁).toReal| < π / 2 :=
  abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)

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