Theorems · Theorem · convex and discrete geometry

ConvexCone.to_isOrderedAddMonoid

∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient),
  have x := C.toPartialOrder h₁ h₂;
  IsOrderedAddMonoid G

A pointed and salient cone defines an IsOrderedAddMonoid.

Defined in

Mathlib.Geometry.Convex.Cone.Basic

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPartialOrderAddCommGroupSMul