Theorems · Definition · order theory

LinearOrder.mkOfAddGroupCone

{S : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommGroup G] →
      [inst_1 : SetLike S G] →
        (C : S) → [AddGroupConeClass S G] → [HasMemOrNegMem C] → [DecidablePred fun x => x ∈ C] → LinearOrder G

Construct a linear order by designating a maximal cone in an abelian group.

Defined in

Mathlib.Algebra.Order.Group.Cone

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

AddCommGroupSetLikeAddGroupConeClassHasMemOrNegMemDecidablePred