Mathlib.Algebra.Order.Monoid.WithTop

WithTop.isOrderedAddMonoid instance

[AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (WithTop α)

Full source

instance isOrderedAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
    IsOrderedAddMonoid (WithTop α) where
  add_le_add_left _ _ := add_le_add_left

Ordered Additive Monoid Structure on $\alpha$ with Top Element

Informal description

For any ordered additive monoid $\alpha$, the type $\alpha$ extended with a top element $\top$ is also an ordered additive monoid, where addition is extended to be monotone with respect to the order and $\top$ is the greatest element.

WithTop.canonicallyOrderedAdd instance

[Add α] [Preorder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedAdd (WithTop α)

Full source

instance canonicallyOrderedAdd [Add α] [Preorder α] [CanonicallyOrderedAdd α] :
    CanonicallyOrderedAdd (WithTop α) :=
  { WithTop.existsAddOfLE with
    le_self_add := fun a b =>
      match a, b with
      | ⊤, ⊤ => le_rfl
      | (a : α), ⊤ => le_top
      | (a : α), (b : α) => WithTop.coe_le_coe.2 le_self_add
      | ⊤, (b : α) => le_rfl }

Canonical Ordering on $\alpha$ Extended with Top Element

Informal description

For any type $\alpha$ with an addition operation and a preorder, if $\alpha$ is a canonically ordered additive monoid, then the type $\alpha$ extended with a top element $\top$ is also a canonically ordered additive monoid.

WithBot.isOrderedAddMonoid instance

[AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (WithBot α)

Full source

instance isOrderedAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
    IsOrderedAddMonoid (WithBot α) :=
  { add_le_add_left := fun _ _ h c => add_le_add_left h c }

Ordered Additive Monoid Structure on $\alpha$ with Bottom Element

Informal description

For any ordered additive monoid $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ is also an ordered additive monoid, where addition is extended to be monotone with respect to the order and $\bot$ is the least element.

WithBot.le_self_add theorem

[Add α] [LE α] [CanonicallyOrderedAdd α] {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) : y ≤ y + x

Full source

protected theorem le_self_add [Add α] [LE α] [CanonicallyOrderedAdd α]
    {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) :
    y ≤ y + x := by
  induction x
  · simp at hx
  induction y
  · simp
  · rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_self_add

Self-Addition Inequality in $\WithBot{\alpha}$ for Canonically Ordered Additive Monoids

Informal description

Let $\alpha$ be a type equipped with an addition operation and a preorder relation, such that $\alpha$ is a canonically ordered additive monoid. For any non-bottom element $x$ in $\WithBot{\alpha}$ (i.e., $x \neq \bot$) and any element $y$ in $\WithBot{\alpha}$, we have $y \leq y + x$.

WithBot.le_add_self theorem

[AddCommMagma α] [LE α] [CanonicallyOrderedAdd α] {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) : y ≤ x + y

Full source

protected theorem le_add_self [AddCommMagma α] [LE α] [CanonicallyOrderedAdd α]
    {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) :
    y ≤ x + y := by
  induction x
  · simp at hx
  induction y
  · simp
  · rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_add_self

Self-Addition Inequality in $\WithBot{\alpha}$ for Canonically Ordered Additive Monoids (Right Version)

Informal description

Let $\alpha$ be a type with an addition operation and a preorder relation, such that $\alpha$ is a canonically ordered additive monoid. For any non-bottom element $x$ in $\WithBot{\alpha}$ (i.e., $x \neq \bot$) and any element $y$ in $\WithBot{\alpha}$, we have $y \leq x + y$.