StrictCombination

📁 Source: Mathlib/Analysis/Convex/StrictCombination.lean

Statistics

Metric	Count
Definitions	0
Theorems dist_lt_of_mem_closedInterior_of_strictConvexSpace, dist_lt_of_mem_interior_of_strictConvexSpace, centerMass_mem_interior, sum_mem_interior, centerMass_mem_ball_of_strictConvexSpace, dist_affineCombination_lt_of_strictConvexSpace, norm_sum_lt_of_strictConvexSpace, sum_mem_ball_of_strictConvexSpace	8
Total	8

Affine.Simplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_lt_of_mem_closedInterior_of_strictConvexSpace 📖	mathematical	Set Set.instMembership closedInterior Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Real.partialOrder Real.instLE Dist.dist PseudoMetricSpace.toDist points	Real.instLT	—	Finset.sum_congr Finset.sum_const_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.affineCombination_affineCombinationSingleWeights Finset.mem_univ Finset.affineCombinationSingleWeights.congr_simp Finset.affineCombinationSingleWeights_apply_self Finset.sum_eq_single Mathlib.Tactic.Push.not_and_eq instIsEmptyFalse Finset.affineCombinationSingleWeights_apply_of_ne dist_affineCombination_lt_of_strictConvexSpace AffineIndependent.injective Real.instNontrivial independent
dist_lt_of_mem_interior_of_strictConvexSpace 📖	mathematical	Set Set.instMembership interior Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Real.partialOrder Real.instLE Dist.dist PseudoMetricSpace.toDist points	Real.instLT	—	dist_lt_of_mem_closedInterior_of_strictConvexSpace Set.mem_of_mem_of_subset interior_subset_closedInterior point_notMem_interior

StrictConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centerMass_mem_interior 📖	mathematical	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finset Finset.instMembership Set Set.instMembership	interior Finset.centerMass	—	Finset.induction instIsEmptyFalse Finset.mem_insert_self Finset.mem_insert_of_mem Finset.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Finset.centerMass_insert zero_add zero_div zero_smul div_self one_smul LT.lt.ne' lt_imp_lt_of_le_of_le le_of_lt le_refl IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le LE.le.lt_of_ne' Finset.sum_nonneg Mathlib.Tactic.Push.not_and_eq Finset.centerMass_congr_fun Finset.centerMass_const strictConvex_iff_div Convex.centerMass_mem convex lt_of_le_of_ne
sum_mem_interior 📖	mathematical	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Finset Finset.instMembership Set Set.instMembership	interior	—	Finset.centerMass_eq_of_sum_1 centerMass_mem_interior

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centerMass_mem_ball_of_strictConvexSpace 📖	mathematical	Real Real.instLE Real.instZero Finset Finset.instMembership Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Metric.ball Finset.centerMass Real.instField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	—	eq_or_ne Metric.ball_zero Metric.closedBall_zero interior_closedBall StrictConvex.centerMass_mem_interior Real.instIsStrictOrderedRing strictConvex_closedBall
dist_affineCombination_lt_of_strictConvexSpace 📖	mathematical	Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Real.instOne Finset Finset.instMembership Dist.dist PseudoMetricSpace.toDist	Real.instLT DFunLike.coe AffineMap Real.instRing Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor AffineMap.instFunLike Finset.affineCombination	—	Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one Finset.weightedVSubOfPoint_apply dist_vadd_left norm_sum_lt_of_strictConvexSpace dist_eq_norm_vsub
norm_sum_lt_of_strictConvexSpace 📖	mathematical	Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Real.instOne Finset Finset.instMembership Norm.norm NormedAddCommGroup.toNorm	Real.instLT ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField	—	mem_ball_zero_iff sum_mem_ball_of_strictConvexSpace
sum_mem_ball_of_strictConvexSpace 📖	mathematical	Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Real.instOne Finset Finset.instMembership Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Metric.ball ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField	—	Finset.centerMass_eq_of_sum_1 centerMass_mem_ball_of_strictConvexSpace

---

← Back to Index