continuousAt_oangle — Mathlib

English

The oriented angle function is continuous at triples where the first point differs from the middle and the last point differs from the middle.

Русский

Функция ориентированного угла непрерывна в тройках точек, если первая точка не совпадает с средней, и последняя точка не совпадает со средней.

LaTeX

$$$\\text{ContinuousAt}\\big(\\lambda y. \\angle y_1 y_2 y_3\\big)\\; x$ при условиях $x_1 \\neq x_2$ и $x_3 \\neq x_2$$$

Lean4

/-- Oriented angles are continuous when neither end point equals the middle point. -/
theorem continuousAt_oangle {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) :
    ContinuousAt (fun y : P × P × P => ∡ y.1 y.2.1 y.2.2) x :=
  by
  unfold oangle
  fun_prop (disch := simp [*])

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