isTangentAt_exsphere_iff_eq_touchpoint

English

The exsphere is tangent to the span of the opposite face at a point p if and only if p is the touchpoint for i.

Русский

Для экссферы равносильно: касание точки p к проломному пространству противоположной грани эквивалентно тому, что p является точкой касания по i.

LaTeX

$$$ (s.exsphere(\text{signs})).IsTangentAt p (\operatorname{affineSpan}_{\mathbb{R}}(\mathrm{range}(s.faceOpposite i).points)) \iff p = s.touchpoint(\text{signs}, i) $$$

Lean4

theorem isTangentAt_exsphere_iff_eq_touchpoint {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs)
    {i : Fin (n + 1)} {p : P} :
    (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint signs i :=
  by
  refine ⟨eq_touchpoint_of_isTangentAt_exsphere, ?_⟩
  rintro rfl
  exact h.isTangentAt_touchpoint i

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