Documentation

Mathlib.Algebra.Order.Sub.WithTop

Lemma about subtraction in ordered monoids with a top element adjoined. #

This file introduces a subtraction on WithTop α when α has a subtraction and a bottom element, given by x - ⊤ = ⊥ and ⊤ - x = ⊤. This will be instantiated mostly for ℕ∞ and ℝ≥0∞, where the bottom element is zero.

Note that there is another subtraction on objects of the form WithTop α in the file Mathlib.Algebra.Order.Group.WithTop, setting -⊤ = ⊤ as this corresponds to the additivization of the usual convention 0⁻¹ = 0 and is relevant in valuation theory. Since this other instance is only registered for LinearOrderedAddCommGroup α (which doesn't have a bottom element, unless the group is trivial), this shouldn't create diamonds.

def WithTop.sub {α : Type u_1} [Sub α] [Bot α] :
WithTop αWithTop αWithTop α

If α has a subtraction and a bottom element, we can extend the subtraction to WithTop α, by setting x - ⊤ = ⊥ and ⊤ - x = ⊤.

Equations
Instances For
    instance WithTop.instSub {α : Type u_1} [Sub α] [Bot α] :
    Equations
    • WithTop.instSub = { sub := WithTop.sub }
    @[simp]
    theorem WithTop.coe_sub {α : Type u_1} [Sub α] [Bot α] {a : α} {b : α} :
    (a - b) = a - b
    @[simp]
    theorem WithTop.top_sub_coe {α : Type u_1} [Sub α] [Bot α] {a : α} :
    - a =
    @[simp]
    theorem WithTop.sub_top {α : Type u_1} [Sub α] [Bot α] {a : WithTop α} :
    a - =
    @[simp]
    theorem WithTop.sub_eq_top_iff {α : Type u_1} [Sub α] [Bot α] {a : WithTop α} {b : WithTop α} :
    a - b = a = b
    theorem WithTop.map_sub {α : Type u_1} {β : Type u_2} [Sub α] [Bot α] [Sub β] [Bot β] {f : αβ} (h : ∀ (x y : α), f (x - y) = f x - f y) (h₀ : f = ) (x : WithTop α) (y : WithTop α) :
    Equations
    • =