Centroid

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Centroid.lean

Statistics

Metric	Count
Definitions `centroid`, `centroidWeights`, `centroidWeightsIndicator`	3
Theorems `centroidWeightsIndicator_def`, `centroidWeights_apply`, `centroidWeights_eq_const`, `centroid_def`, `centroid_eq_affineCombination_fintype`, `centroid_eq_centroid_image_of_inj_on`, `centroid_eq_of_inj_on_of_image_eq`, `centroid_map`, `centroid_pair`, `centroid_pair_fin`, `centroid_singleton`, `centroid_univ`, `centroid_vsub_const`, `sum_centroidWeightsIndicator`, `sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one`, `sum_centroidWeightsIndicator_eq_one_of_card_ne_zero`, `sum_centroidWeightsIndicator_eq_one_of_nonempty`, `sum_centroidWeights_eq_one_of_card_eq_add_one`, `sum_centroidWeights_eq_one_of_card_ne_zero`, `sum_centroidWeights_eq_one_of_cast_card_ne_zero`, `sum_centroidWeights_eq_one_of_nonempty`, `centroid_mem_affineSpan_of_card_eq_add_one`, `centroid_mem_affineSpan_of_card_ne_zero`, `centroid_mem_affineSpan_of_cast_card_ne_zero`, `centroid_mem_affineSpan_of_nonempty`	25
Total	28

Finset

Definitions

Name	Category	Theorems
`centroid` 📖	CompOp	30 math math: `centroid_eq_affineCombination_fintype`, `Affine.Simplex.face_centroid_eq_iff`, `Affine.Simplex.univ_centroid_eq`, `Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter`, `Affine.Simplex.centroid_eq_of_range_eq`, `Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub`, `centroid_map`, `Affine.Simplex.face_centroid_eq_centroid`, `Affine.Simplex.mongePlane_def`, `centroid_mem_affineSpan_of_nonempty`, `centroid_univ`, `centroid_eq_centerMass`, `centroid_mem_affineSpan_of_cast_card_ne_zero`, `AffineBasis.coord_apply_centroid`, `Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter`, `centroid_mem_convexHull`, `centroid_vsub_const`, `centroid_singleton`, `centroid_eq_centroid_image_of_inj_on`, `Affine.Simplex.centroid_eq_iff`, `Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter`, `centroid_pair`, `centroid_pair_fin`, `centroid_mem_affineSpan_of_card_eq_add_one`, `centroid_eq_of_inj_on_of_image_eq`, `AffineBasis.centroid_mem_interior_convexHull`, `centroid_mem_affineSpan_of_card_ne_zero`, `Affine.Simplex.circumcenter_eq_centroid`, `centroid_def`, `Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter`
`centroidWeights` 📖	CompOp	11 math math: `sum_centroidWeights_eq_one_of_card_eq_add_one`, `centroidWeights_apply`, `sum_centroidWeights_eq_one_of_card_ne_zero`, `centroid_eq_centerMass`, `sum_centroidWeightsIndicator`, `centroidWeightsIndicator_def`, `sum_centroidWeights_eq_one_of_nonempty`, `Affine.Simplex.centroid_eq_affineCombination`, `centroidWeights_eq_const`, `sum_centroidWeights_eq_one_of_cast_card_ne_zero`, `centroid_def`
`centroidWeightsIndicator` 📖	CompOp	6 math math: `sum_centroidWeightsIndicator_eq_one_of_nonempty`, `centroid_eq_affineCombination_fintype`, `sum_centroidWeightsIndicator_eq_one_of_card_ne_zero`, `sum_centroidWeightsIndicator`, `sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one`, `centroidWeightsIndicator_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centroidWeightsIndicator_def` 📖	mathematical	—	`centroidWeightsIndicator` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `SetLike.coe` `Finset` `instSetLike` `centroidWeights`	—	—
`centroidWeights_apply` 📖	mathematical	—	`centroidWeights` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `card`	—	—
`centroidWeights_eq_const` 📖	mathematical	—	`centroidWeights` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `card`	—	—
`centroid_def` 📖	mathematical	—	`centroid` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `instAddTorsorForall` `AffineMap.instFunLike` `affineCombination` `centroidWeights`	—	—
`centroid_eq_affineCombination_fintype` 📖	mathematical	—	`centroid` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `instAddTorsorForall` `AffineMap.instFunLike` `affineCombination` `univ` `centroidWeightsIndicator`	—	`affineCombination_indicator_subset` `subset_univ`
`centroid_eq_centroid_image_of_inj_on` 📖	mathematical	`Set.image` `SetLike.coe` `Finset` `instSetLike`	`centroid` `Set.Elem` `univ` `Set` `Set.instMembership`	—	`ext` `mem_map` `Set.mem_image_of_mem` `mem_univ` `centroid_map`
`centroid_eq_of_inj_on_of_image_eq` 📖	mathematical	`Set.image` `SetLike.coe` `Finset` `instSetLike`	`centroid`	—	`centroid_eq_centroid_image_of_inj_on`
`centroid_map` 📖	mathematical	—	`centroid` `map` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`card_map` `affineCombination_map`
`centroid_pair` 📖	mathematical	—	`centroid` `Finset` `instInsert` `instSingleton` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.instAtLeastTwoHAddOfNat` `VSub.vsub` `AddTorsor.toVSub`	—	`Nat.instAtLeastTwoHAddOfNat` `insert_eq_of_mem` `centroid_singleton` `vsub_self` `smul_zero` `zero_vadd` `card_insert_of_notMem` `notMem_singleton` `card_singleton` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Invertible.ne_zero` `DivisionRing.toNontrivial` `centroid_def` `affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` `sum_centroidWeights_eq_one_of_cast_card_ne_zero` `weightedVSubOfPoint_insert` `weightedVSubOfPoint_apply` `sum_congr` `one_add_one_eq_two` `sum_singleton`
`centroid_pair_fin` 📖	mathematical	—	`centroid` `univ` `Fin.fintype` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.instAtLeastTwoHAddOfNat` `VSub.vsub` `AddTorsor.toVSub`	—	`Nat.instAtLeastTwoHAddOfNat` `univ_fin2` `centroid_pair`
`centroid_singleton` 📖	mathematical	—	`centroid` `Finset` `instSingleton`	—	`AddTorsor.nonempty` `weightedVSubOfPoint_apply` `sum_congr` `card_singleton` `Nat.cast_one` `inv_one` `one_smul` `sum_singleton` `vsub_vadd`
`centroid_univ` 📖	mathematical	—	`centroid` `Finset` `SetLike.instMembership` `instSetLike` `univ` `Subtype.fintype`	—	`centroid.eq_1` `attach_affineCombination_coe` `card_attach`
`centroid_vsub_const` 📖	mathematical	`Nonempty`	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `centroid` `addGroupIsAddTorsor`	—	`sum_centroidWeights_eq_one_of_nonempty`
`sum_centroidWeightsIndicator` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `univ` `centroidWeightsIndicator` `centroidWeights`	—	`sum_indicator_subset` `subset_univ`
`sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one` 📖	mathematical	`card`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `univ` `centroidWeightsIndicator` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_centroidWeightsIndicator` `sum_centroidWeights_eq_one_of_card_eq_add_one`
`sum_centroidWeightsIndicator_eq_one_of_card_ne_zero` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `univ` `centroidWeightsIndicator` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_centroidWeightsIndicator` `sum_centroidWeights_eq_one_of_card_ne_zero`
`sum_centroidWeightsIndicator_eq_one_of_nonempty` 📖	mathematical	`Nonempty`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `univ` `centroidWeightsIndicator` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_centroidWeightsIndicator` `sum_centroidWeights_eq_one_of_nonempty`
`sum_centroidWeights_eq_one_of_card_eq_add_one` 📖	mathematical	`card`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `centroidWeights` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_centroidWeights_eq_one_of_card_ne_zero`
`sum_centroidWeights_eq_one_of_card_ne_zero` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `centroidWeights` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_congr` `sum_const` `nsmul_eq_mul` `mul_inv_cancel₀`
`sum_centroidWeights_eq_one_of_cast_card_ne_zero` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `centroidWeights` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_congr` `sum_const` `nsmul_eq_mul` `mul_inv_cancel₀`
`sum_centroidWeights_eq_one_of_nonempty` 📖	mathematical	`Nonempty`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `centroidWeights` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sum_centroidWeights_eq_one_of_card_ne_zero` `ne_of_gt` `card_pos`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centroid_mem_affineSpan_of_card_eq_add_one` 📖	mathematical	`Finset.card`	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `Finset.centroid`	—	`affineCombination_mem_affineSpan` `instNontrivialOfCharZero` `Finset.sum_centroidWeights_eq_one_of_card_eq_add_one`
`centroid_mem_affineSpan_of_card_ne_zero` 📖	mathematical	—	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `Finset.centroid`	—	`affineCombination_mem_affineSpan` `instNontrivialOfCharZero` `Finset.sum_centroidWeights_eq_one_of_card_ne_zero`
`centroid_mem_affineSpan_of_cast_card_ne_zero` 📖	mathematical	—	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `Finset.centroid`	—	`affineCombination_mem_affineSpan` `DivisionRing.toNontrivial` `Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero`
`centroid_mem_affineSpan_of_nonempty` 📖	mathematical	`Finset.Nonempty`	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `Finset.centroid`	—	`affineCombination_mem_affineSpan` `instNontrivialOfCharZero` `Finset.sum_centroidWeights_eq_one_of_nonempty`

---

← Back to Index