continuousAt_angle — Mathlib

English

If a triple of points x=(a,b,c) in P^3 has a ≠ b and c ≠ b, then the map y ↦ ∠ y1 y2 y3 is continuous at x.

Русский

Если у тройки точек x=(a,b,c) в P^3 выполняются a ≠ b и c ≠ b, то отображение y ↦ ∠ y1 y2 y3 непрерывно в точке x.

LaTeX

$$$\text{ContinuousAt}_{(a,b,c)}( y\mapsto \angle y_1 y_2 y_3 )$ при $a\neq b$ и $c\neq b$.$$

Lean4

theorem continuousAt_angle {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
  let f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
  have hf1 : (f x).1 ≠ 0 := by simp [f, hx12]
  have hf2 : (f x).2 ≠ 0 := by simp [f, hx32]
  exact (InnerProductGeometry.continuousAt_angle hf1 hf2).comp (by fun_prop)

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