Theorems · Inductive type · convex and discrete geometry

Convexity.IsModuleConvexSpace

(R : Type u_2) →
  (M : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsStrictOrderedRing R] →
          [inst_3 : AddCommMonoid M] → [Module R M] → [Convexity.ConvexSpace R M] → Prop

Typeclass for a convex space structure on a module to be given by weighted sums.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Module

Cited by

20 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

SemiringPartialOrderIsStrictOrderedRingAddCommMonoidModuleConvexity.ConvexSpace