Theorems · Theorem · geometry

Finset.centroid_eq_of_inj_on_of_image_eq

∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {ι₂ : Type u_5} (s₂ : Finset ι₂) {p : ι → P},
  (∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) →
    ∀ {p₂ : ι₂ → P},
      (∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j) → p '' ↑s = p₂ '' ↑s₂ → Finset.centroid k s p = Finset.centroid k s₂ p₂

Two indexed families of points that are injective on the given Finsets and with the same points in the image of those Finsets have the same centroid.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Centroid

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleAddTorsor