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

ink

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

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

ink

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

Equations

• WithTop.instSubWithTop = { sub := WithTop.sub }

ink

@[simp]

theorem WithTop.coe_sub {α : Type u_1} [inst : Sub α] [inst : Zero α] {a : α} {b : α} : ↑(a - b) = ↑a - ↑b

ink

@[simp]

theorem WithTop.top_sub_coe {α : Type u_1} [inst : Sub α] [inst : Zero α] {a : α} : ⊤ - ↑a = ⊤

ink

@[simp]

theorem WithTop.sub_top {α : Type u_1} [inst : Sub α] [inst : Zero α] {a : WithTop α} : a - ⊤ = 0

ink

@[simp]

theorem WithTop.sub_eq_top_iff {α : Type u_1} [inst : Sub α] [inst : Zero α] {a : WithTop α} {b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

ink

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

ink

instance WithTop.instOrderedSubWithTopToLEPreorderToPreorderToPartialOrderToOrderedAddCommMonoidAddToAddToAddZeroClassToAddMonoidToAddCommMonoidInstSubWithTopToZero {α : Type u_1} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] : OrderedSub (WithTop α)

Equations

• One or more equations did not get rendered due to their size.