Documentation

Mathlib.Algebra.Order.Sub.WithTop

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

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

If α has subtraction and 0, we can extend the subtraction to WithTop α.

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