Theorems · Inductive type · convex and discrete geometry

ConvexCone

(R : Type u_2) → (M : Type u_4) → [Semiring R] → [PartialOrder R] → [AddCommMonoid M] → [SMul R M] → Type u_4

A convex cone is a subset s of an R-module such that a • x + b • y ∈ s whenever a, b > 0 and x, y ∈ s.

Defined in

Mathlib.Geometry.Convex.Cone.Basic

Cited by

103 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 5 definitions · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidSMul