Documentation

Mathlib.Algebra.Order.Group.Cone

Construct ordered groups from positive cones #

In this file we provide structures PositiveCone and TotalPositiveCone that encode axioms of OrderedAddCommGroup and LinearOrderedAddCommGroup in terms of the (0 ≤ ·) predicate.

We also provide two constructors, OrderedAddCommGroup.mkOfPositiveCone and LinearOrderedAddCommGroup.mkOfPositiveCone, that turn these structures into instances of the corresponding typeclasses.

structure AddCommGroup.PositiveCone (α : Type u_1) [AddCommGroup α] :
Type u_1

A collection of elements in an AddCommGroup designated as "non-negative". This is useful for constructing an OrderedAddCommGroup by choosing a positive cone in an existing AddCommGroup.

  • nonneg : αProp

    The characteristic predicate of a positive cone. nonneg a means that 0 ≤ a according to the cone.

  • pos : αProp

    The characteristic predicate of a positive cone. pos a means that 0 < a according to the cone.

  • pos_iff : ∀ (a : α), self.pos a self.nonneg a ¬self.nonneg (-a)
  • zero_nonneg : self.nonneg 0
  • add_nonneg : ∀ {a b : α}, self.nonneg aself.nonneg bself.nonneg (a + b)
  • nonneg_antisymm : ∀ {a : α}, self.nonneg aself.nonneg (-a)a = 0
Instances For
    theorem AddCommGroup.PositiveCone.pos_iff {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) (a : α) :
    self.pos a self.nonneg a ¬self.nonneg (-a)
    theorem AddCommGroup.PositiveCone.add_nonneg {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) {a : α} {b : α} :
    self.nonneg aself.nonneg bself.nonneg (a + b)
    theorem AddCommGroup.PositiveCone.nonneg_antisymm {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) {a : α} :
    self.nonneg aself.nonneg (-a)a = 0

    A positive cone in an AddCommGroup induces a linear order if for every a, either a or -a is non-negative.

    • nonneg : αProp
    • pos : αProp
    • pos_iff : ∀ (a : α), self.pos a self.nonneg a ¬self.nonneg (-a)
    • zero_nonneg : self.nonneg 0
    • add_nonneg : ∀ {a b : α}, self.nonneg aself.nonneg bself.nonneg (a + b)
    • nonneg_antisymm : ∀ {a : α}, self.nonneg aself.nonneg (-a)a = 0
    • nonnegDecidable : DecidablePred self.nonneg

      For any a the proposition nonneg a is decidable

    • nonneg_total : ∀ (a : α), self.nonneg a self.nonneg (-a)

      Either a or -a is nonneg

    Instances For
      theorem AddCommGroup.TotalPositiveCone.nonneg_total {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.TotalPositiveCone α) (a : α) :
      self.nonneg a self.nonneg (-a)

      Either a or -a is nonneg

      Construct an OrderedAddCommGroup by designating a positive cone in an existing AddCommGroup.

      Equations
      Instances For

        Construct a LinearOrderedAddCommGroup by designating a positive cone in an existing AddCommGroup such that for every a, either a or -a is non-negative.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For