mongePoint_mem_affineSpan — Mathlib

English

If two simplices s1 and s2 have the same set of vertices, then their Monge points coincide.

Русский

Если два симплекса имеют один и тот же набор вершин, их MongePoint совпадает.

LaTeX

$$$$ \text{If } \mathrm{range}(s_1.points) = \mathrm{range}(s_2.points), \ s_1.mongePoint = s_2.mongePoint. $$$$

Lean4

/-- The Monge point lies in the affine span. -/
theorem mongePoint_mem_affineSpan {n : ℕ} (s : Simplex ℝ P n) : s.mongePoint ∈ affineSpan ℝ (Set.range s.points) :=
  smul_vsub_vadd_mem _ _ (centroid_mem_affineSpan_of_card_eq_add_one ℝ _ (card_fin (n + 1)))
    s.circumcenter_mem_affineSpan s.circumcenter_mem_affineSpan

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