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/AddGroupWithTop.lean, setting -⊤ = ⊤ as this corresponds to the additivization of the usual convention 0⁻¹ = 0 and is relevant in valuation theory. Since that other instance is only registered for AddCommGroup α (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 = ⊤.

@[instance_reducible]

instance WithTop.instSub {α : Type u_1} [Sub α] [Bot α] : Sub (WithTop α)

@[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 b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem WithTop.sub_ne_top_iff {α : Type u_1} [Sub α] [Bot α] {a 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 y : WithTop α) : map f (x - y) = map f x - map f y

instance WithTop.instOrderedSub {α : Type u_1} [Add α] [LE α] [OrderBot α] [Sub α] [OrderedSub α] : OrderedSub (WithTop α)