centroid_mem_interior_convexHull — Mathlib

English

The centroid of a finite affine basis lies in the interior of the convex hull of the basis range.

Русский

Центроид конечной аффинной базы лежит внутри выпуклой оболочки базы.

LaTeX

$$$$\text{Finset.univ.centroid}_{\mathbb{R}}(b) \in \operatorname{int}(\operatorname{convexHull}_{\mathbb{R}}(\operatorname{range}(b))).$$$$

Lean4

theorem centroid_mem_interior_convexHull {ι} [Fintype ι] (b : AffineBasis ι ℝ V) :
    Finset.univ.centroid ℝ b ∈ interior (convexHull ℝ (range b)) :=
  by
  haveI := b.nonempty
  simp only [b.interior_convexHull, mem_setOf_eq, b.coord_apply_centroid (Finset.mem_univ _), inv_pos, Nat.cast_pos,
    Finset.card_pos, Finset.univ_nonempty, forall_true_iff]

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