Structures · Geometry
Convexity.ConvexSpace
A set equipped with an operation of finite convex combinations, where the coefficients must be non-negative and sum to 1.
- Defined in
- Mathlib.Geometry.Convex.ConvexSpace.Defs
- Shape
- 2 explicit arguments · adds sConvexComb, sConvexComb_single, assoc
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by194
- Convexity.ConvexSpace.sConvexComb
- Convexity.convexCombPair
- Convexity.iConvexComb
- Convexity.IsConvexSet
- Convexity.convexHull
- Convexity.IsStarConvexSet
- Convexity.convexCombPair.congr_simp
- Convexity.iConvexComb_congr
- Convexity.iConvexComb_eq_sum
- Convexity.ConvexSpace.sConvexComb_single
- Convexity.IsAffineMap.map_convexCombPair
- Convexity.IsAffineMap.map_iConvexComb
- Convexity.iConvexComb_const
- Convexity.ConvexSpace.AffineMap.comp
- Convexity.IsAffineMap.map_sConvexComb
- Convexity.iConvexComb_id'
- Convexity.dist_iConvexComb_le
- Convexity.IsConvexSet.sConvexComb_mem
- Convexity.sConvexComb_sConvexComb
- Convexity.ConvexSpace.subtype
- Prod.isAffineMap_fst
- Convexity.dist_convexCombPair_left
- Convexity.IsConvexSet.convexHull_eq_self
- Prod.isAffineMap_snd
- Convexity.convexCombPair_symm
- Convexity.IsStarConvexSet.image
- Convexity.convexCombPair_one
- Convexity.IsConvexSet.sInter
- Convexity.ConvexSpace.AffineMap.id
- Convexity.continuous_convexCombPair
- Convexity.dist_convexCombPair_convexCombPair_le
- Convexity.IsStarConvexSet.prod
- Convexity.convexCombPair_iConvexComb_iConvexComb
- Convexity.iConvexComb_assoc'
- Convexity.convexCombPair_zero
- Convexity.iConvexComb_convexCombPair_comm
- Convexity.convexCombPair_same
- Convexity.isConvexSet_coe
- Convexity.IsAffineMap.add
- Finsupp.isAffineMap_eval
- Convexity.IsConvexSet.empty
- Convexity.IsAffineMap.neg
- Pi.isAffineMap_eval
- Convexity.convexCombPair_def
- Convexity.IsConvexSet.convexHull_subset_iff
- Convexity.dist_convexCombPair_right
- Convexity.isAffineMap_subtypeVal
- Convexity.IsAffineMap.map_sum_weights
- Convexity.subset_convexHull_self
- Convexity.iConvexComb_map
Ancestors0
No ancestors.