Documentation

Mathlib.Algebra.Order.Sub.WithTop

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

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

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

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