# mathlib3documentation

algebra.order.sub.with_top

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected]
def with_top.sub {α : Type u_1} [has_sub α] [has_zero α] (a b : with_top α) :

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

Equations
@[protected, instance]
def with_top.has_sub {α : Type u_1} [has_sub α] [has_zero α] :
Equations
@[simp, norm_cast]
theorem with_top.coe_sub {α : Type u_1} [has_sub α] [has_zero α] {a b : α} :
(a - b) = a - b
@[simp]
theorem with_top.top_sub_coe {α : Type u_1} [has_sub α] [has_zero α] {a : α} :
@[simp]
theorem with_top.sub_top {α : Type u_1} [has_sub α] [has_zero α] {a : with_top α} :
a - = 0
@[simp]
theorem with_top.sub_eq_top_iff {α : Type u_1} [has_sub α] [has_zero α] {a b : with_top α} :
a - b = a = b
theorem with_top.map_sub {α : Type u_1} {β : Type u_2} [has_sub α] [has_zero α] [has_sub β] [has_zero β] {f : α β} (h : (x y : α), f (x - y) = f x - f y) (h₀ : f 0 = 0) (x y : with_top α) :
(x - y) = x - y
@[protected, instance]
def with_top.has_ordered_sub {α : Type u_1} [has_sub α]  :