excenter_singleton_mem_affineSpan_range

English

The excenter with given signs lies in the affine span of the vertex range of s.

Русский

Экцентер с данным набором знаков лежит в афинном замещении множества вершин s.

LaTeX

$$s.excenter signs ∈ affineSpan ℝ (Set.range s.points)$$

Lean4

theorem excenter_singleton_mem_affineSpan_range [Nat.AtLeastTwo n] (i : Fin (n + 1)) :
    s.excenter { i } ∈ affineSpan ℝ (Set.range s.points) :=
  (s.excenterExists_singleton i).excenter_mem_affineSpan_range

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