scilib documentation

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.

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

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

Equations
source
@[protected, instance]
def with_top.has_sub {α : Type u_1} [has_sub α] [has_zero α] :
has_sub (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_sub {α : Type u_1} [has_sub α] [has_zero α] {a b : α} :
↑(a - b) = ↑a - ↑b
source
@[simp]
theorem with_top.top_sub_coe {α : Type u_1} [has_sub α] [has_zero α] {a : α} :
⊤ - ↑a = ⊤
source
@[simp]
theorem with_top.sub_top {α : Type u_1} [has_sub α] [has_zero α] {a : with_top α} :
a - ⊤ = 0
source
@[simp]
theorem with_top.sub_eq_top_iff {α : Type u_1} [has_sub α] [has_zero α] {a b : with_top α} :
a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
source
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 α) :
with_top.map f (x - y) = with_top.map f x - with_top.map f y
source
@[protected, instance]
def with_top.has_ordered_sub {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] :
has_ordered_sub (with_top α)