Theorems · Theorem · convex and discrete geometry
Finset.centroid_eq_centerMass
∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
[inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι),
s.Nonempty → ∀ (p : ι → E), Finset.centroid R s p = s.centerMass (Finset.centroidWeights R s) pThe centroid can be regarded as a center of mass.
- Defined in
- Mathlib.Analysis.Convex.Combination
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Finsetstatement and proof · cited by 13,712
- AddCommGroupstatement and proof · cited by 12,871
- LinearOrderstatement and proof · cited by 8,572
- Fieldstatement and proof · cited by 7,404
- IsStrictOrderedRingstatement and proof · cited by 2,490
- Finset.Nonemptystatement and proof · cited by 1,001
- Finset.centerMassstatement · cited by 49
- Finset.centroidstatement · cited by 45
- Finset.centroidWeightsstatement · cited by 27
- Finset.sum_centroidWeights_eq_one_of_nonemptyproof · cited by 8
- affineCombination_eq_centerMassproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- exists_mem_interior_convexHull_affineBasisproof · cited by 2
- Finset.centroid_mem_convexHullproof · cited by 0