centroid_singleton — Mathlib

English

The centroid of a singleton is the single point: centroid of {i} with p is p(i).

Русский

Центроид одиночного множества {i} равен самой точке: centroid = p(i).

LaTeX

$$$({\\,i\\})\\in \\text{Finset }\\iota: \\; (\\{i\\} ).\\mathrm{centroid}(k,p) = p(i)$$$

Lean4

/-- The centroid of a single point. -/
@[simp]
theorem centroid_singleton (p : ι → P) (i : ι) : ({ i } : Finset ι).centroid k p = p i := by
  simp [centroid_def, affineCombination_apply]

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