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

• x.sub none = ↑⊥
• WithTop.sub none (some x_2) = ⊤
• WithTop.sub (some x_2) (some y) = ↑(x_2 - y)

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

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 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 α) : WithTop.map f (x - y) = WithTop.map f x - WithTop.map f y

theorem WithTop.instOrderedSub {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] : OrderedSub (WithTop α)