English
If the image sets of p on s and q on t coincide, then their centroids coincide.
Русский
Если образы p на s и q на t совпадают, то их центроиды совпадают.
LaTeX
$$$\\mathrm{Set.image}\\ p\ \ s = \\mathrm{Set.image}\\ q\ \ t \\Rightarrow \\mathrm{centroid}(k,s,p) = \\mathrm{centroid}(k,t,q)$$$
Lean4
/-- Two indexed families of points that are injective on the given
`Finset`s and with the same points in the image of those `Finset`s
have the same centroid. -/
theorem centroid_eq_of_inj_on_of_image_eq {p : ι → P} (hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) {p₂ : ι₂ → P}
(hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j) (he : p '' ↑s = p₂ '' ↑s₂) : s.centroid k p = s₂.centroid k p₂ := by
classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl, s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]