face_centroid_eq_centroid — Mathlib

English

The centroid of a face equals the centroid of the corresponding subset of vertices.

Русский

Центроид грани равен центроиду соответствующего подмножества вершин.

LaTeX

$$$\text{Finset.univ.centroid}(k)\; (s.face h).points = fs.centroid(k)\; s.points$$$

Lean4

/-- The centroid of a face of a simplex as the centroid of a subset of
the points. -/
@[simp]
theorem face_centroid_eq_centroid {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) :
    Finset.univ.centroid k (s.face h).points = fs.centroid k s.points :=
  by
  convert (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm
  rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]
  simp

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