Mathlib.Algebra.Order.Sub.WithTop

Module docstring

{"# 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. "}

WithTop.sub definition

: ∀ _ _ : WithTop α, WithTop α

Full source

/-- If `α` has a subtraction and a bottom element, we can extend the subtraction to `WithTop α`, by
setting `x - ⊤ = ⊥` and `⊤ - x = ⊤`. -/
protected def sub : ∀ _ _ : WithTop α, WithTop α
  | _, ⊤ => (⊥ : α)
  | ⊤, (x : α) => ⊤
  | (x : α), (y : α) => (x - y : α)

Subtraction on a type extended with a top element

Informal description

The subtraction operation on the type `WithTop α` (where `α` is a type with a subtraction operation and a bottom element `⊥`) is defined as follows: - For any element $x$ in `WithTop α`, $x - \top = \bot$. - For any element $x$ in `WithTop α$, $\top - x = \top$. - For elements $x, y$ in $\alpha$, the subtraction is defined as the usual subtraction in $\alpha$.

WithTop.instSub instance

: Sub (WithTop α)

Full source

instance : Sub (WithTop α) :=
  ⟨WithTop.sub⟩

Subtraction on $\text{WithTop}\,\alpha$ with Top and Bottom Elements

Informal description

For any type $\alpha$ with a subtraction operation and a bottom element $\bot$, the type $\text{WithTop}\,\alpha$ (obtained by adjoining a top element $\top$ to $\alpha$) has a subtraction operation defined by: - $x - \top = \bot$ for any $x \in \text{WithTop}\,\alpha$, - $\top - x = \top$ for any $x \in \text{WithTop}\,\alpha$, - For $x, y \in \alpha$, the subtraction is inherited from $\alpha$.

WithTop.coe_sub theorem

{a b : α} : (↑(a - b) : WithTop α) = ↑a - ↑b

Full source

@[simp, norm_cast]
theorem coe_sub {a b : α} : (↑(a - b) : WithTop α) = ↑a - ↑b :=
  rfl

Subtraction Commutes with Injection into $\text{WithTop}\,\alpha$

Informal description

For any elements $a, b$ in a type $\alpha$ with a subtraction operation and a bottom element $\bot$, the canonical injection of their difference into $\text{WithTop}\,\alpha$ equals the difference of their injections, i.e., $\uparrow(a - b) = \uparrow a - \uparrow b$.

WithTop.top_sub_coe theorem

{a : α} : (⊤ : WithTop α) - a = ⊤

Full source

@[simp]
theorem top_sub_coe {a : α} : (⊤ : WithTop α) - a = ⊤ :=
  rfl

Subtraction from Top in $\text{WithTop}\,\alpha$ Yields Top

Informal description

For any element $a$ of type $\alpha$, the subtraction of the image of $a$ in $\text{WithTop}\,\alpha$ from the top element $\top$ equals $\top$, i.e., $\top - a = \top$.

WithTop.sub_top theorem

{a : WithTop α} : a - ⊤ = (⊥ : α)

Full source

@[simp]
theorem sub_top {a : WithTop α} : a - ⊤ = (⊥ : α) := by cases a <;> rfl

Subtraction of Top Element Yields Bottom in $\text{WithTop}\,\alpha$

Informal description

For any element $a$ in the type $\text{WithTop}\,\alpha$ (where $\alpha$ is a type with a subtraction operation and a bottom element $\bot$), the subtraction $a - \top$ equals the bottom element $\bot$.

WithTop.sub_eq_top_iff theorem

{a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Full source

@[simp] theorem sub_eq_top_iff {a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤ := by
  induction a <;> induction b <;>
    simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, top_sub_coe, false_and, Ne,
      not_true_eq_false, not_false_eq_true, and_false, and_self]

Characterization of Top Subtraction in $\text{WithTop}\,\alpha$: $a - b = \top \leftrightarrow (a = \top \land b \neq \top)$

Informal description

For any elements $a, b$ in the type $\text{WithTop}\,\alpha$ (where $\alpha$ has a subtraction operation and a bottom element $\bot$), the subtraction $a - b$ equals the top element $\top$ if and only if $a = \top$ and $b \neq \top$.

WithTop.sub_ne_top_iff theorem

{a b : WithTop α} : a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

Full source

lemma sub_ne_top_iff {a b : WithTop α} : a - b ≠ ⊤a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤ := by simp [or_iff_not_imp_left]

Characterization of Non-Top Subtraction in $\text{WithTop}\,\alpha$: $a - b \neq \top \leftrightarrow (a \neq \top \lor b = \top)$

Informal description

For any elements $a, b$ in the type $\text{WithTop}\,\alpha$ (where $\alpha$ is a type with a subtraction operation and a bottom element $\bot$), the subtraction $a - b$ is not equal to the top element $\top$ if and only if either $a$ is not equal to $\top$ or $b$ is equal to $\top$.

WithTop.map_sub theorem

 [Sub β] [Bot β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y) (h₀ : f ⊥ = ⊥) :
  ∀ x y : WithTop α, (x - y).map f = x.map f - y.map f

Full source

protected
theorem map_sub [Sub β] [Bot β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y) (h₀ : f ⊥ = ⊥) :
    ∀ x y : WithTop α, (x - y).map f = x.map f - y.map f
  | _, ⊤ => by simp only [sub_top, map_coe, h₀, map_top]
  | ⊤, (x : α) => rfl
  | (x : α), (y : α) => by simp only [← coe_sub, map_coe, h]

Preservation of Subtraction under Lifted Maps in $\text{WithTop}\,\alpha$

Informal description

Let $\alpha$ and $\beta$ be types equipped with subtraction operations and bottom elements $\bot$. Given a function $f : \alpha \to \beta$ such that: 1. $f$ preserves subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in \alpha$, 2. $f$ maps the bottom element to the bottom element: $f(\bot) = \bot$, then for any $x, y \in \text{WithTop}\,\alpha$, the following equality holds: $$(x - y).\text{map}\,f = x.\text{map}\,f - y.\text{map}\,f.$$ Here, $\text{map}\,f$ denotes the lifting of $f$ to $\text{WithTop}\,\alpha \to \text{WithTop}\,\beta$ that applies $f$ to elements of $\alpha$ and preserves the top element $\top$.

WithTop.instOrderedSub instance

: OrderedSub (WithTop α)

Full source

instance : OrderedSub (WithTop α) := by
  constructor
  rintro x y z
  cases y
  · cases z <;> simp
  cases x
  · simp
  cases z
  · simp
  norm_cast
  exact tsub_le_iff_right

Ordered Subtraction Structure on $\text{WithTop}\,\alpha$ with Top and Bottom Elements

Informal description

For any type $\alpha$ with a subtraction operation, a bottom element $\bot$, and an ordered subtraction structure, the type $\text{WithTop}\,\alpha$ (obtained by adjoining a top element $\top$ to $\alpha$) also has an ordered subtraction structure. This structure is defined by: - $x - \top = \bot$ for any $x \in \text{WithTop}\,\alpha$, - $\top - x = \top$ for any $x \in \text{WithTop}\,\alpha$, - For $x, y \in \alpha$, the subtraction is inherited from $\alpha$. Moreover, this subtraction satisfies the ordered subtraction property: for any $a, b, c \in \text{WithTop}\,\alpha$, the inequality $a - b \leq c$ holds if and only if $a \leq c + b$.