centroid_eq_of_inj_on_of_image_eq

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]

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