Structures · Geometry
Convexity.IsModuleConvexSpace
Typeclass for a convex space structure on a module to be given by weighted sums.
- Shape
- 2 explicit arguments · adds sConvexComb_eq_sum
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 by25
- Convexity.iConvexComb_eq_sum
- Convexity.IsModuleConvexSpace.sConvexComb_eq_sum
- Convexity.isConvexSet_coe
- Convexity.IsAffineMap.add
- Convexity.IsAffineMap.neg
- Convexity.IsAffineMap.map_sum_weights
- Convexity.IsAffineMap.fun_add
- Convexity.IsAffineMap.sub
- Convexity.IsAffineMap.fun_sub
- Convexity.IsAffineMap.fun_neg
- Convexity.convexCombPair_eq_sum
- Convexity.instIsModuleConvexSpaceForall
- Convexity.instIsModuleConvexSpaceSubtypeMem
- Convexity.IsStarConvexSet.add
- Convexity.subtypeVal_submodule_sConvexComb
- Convexity.IsStarConvexSet.neg
- Convexity.IsStarConvexSet.sub
- Convexity.instIsModuleConvexSpaceProd
- Convexity.subtypeVal_submodule_convexCombPair
- Convexity.IsConvexDist.submodule
- convexCombination_eq_sum
- Convexity.IsAffineMap.map_smul_add_smul
- Convexity.instIsModuleConvexSpaceFinsupp
- Convexity.instConvexSpaceSubtypeMem
- Convexity.subtypeVal_submodule_iConvexComb
Ancestors0
No ancestors.