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

• WithTop.sub x✝ x = match x✝, x with | x, none => 0 | none, some x => ⊤ | some x, some y => ↑(x - y)

instance WithTop.instSubWithTop {α : Type u_1} [Sub α] [Zero α] : Sub (WithTop α)

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

instance WithTop.instOrderedSubWithTopToLEPreorderToPreorderToPartialOrderToOrderedAddCommMonoidAddToAddToAddCommMagmaToAddCommSemigroupToAddCommMonoidInstSubWithTopToZeroToAddMonoid {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] : OrderedSub (WithTop α)

Equations

• (_ : OrderedSub (WithTop α)) = (_ : OrderedSub (WithTop α))