doc-next-gen

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Module docstring

{"# Adjoining top/bottom elements to ordered monoids. "}

WithTop.one instance
: One (WithTop α)
Full source 
@[to_additive]
instance one : One (WithTop α) :=
  ⟨(1 : α)⟩
One Element in `WithTop α`
Informal description
The type `WithTop α` has a canonical one element when `α` has a one element. Specifically, the one element of `WithTop α` is the image of the one element of `α` under the canonical injection `WithTop.some`.
WithTop.coe_one theorem
: ((1 : α) : WithTop α) = 1
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_one : ((1 : α) : WithTop α) = 1 :=
  rfl
Injection of One Preserves Identity in $\text{WithTop}\ \alpha$
Informal description
The canonical injection of the multiplicative identity $1$ from a type $\alpha$ into $\text{WithTop}\ \alpha$ is equal to the multiplicative identity in $\text{WithTop}\ \alpha$. In symbols, $(1 : \text{WithTop}\ \alpha) = 1$.
WithTop.coe_eq_one theorem
: (a : WithTop α) = 1 ↔ a = 1
Full source 
@[to_additive (attr := simp, norm_cast)]
lemma coe_eq_one : (a : WithTop α) = 1 ↔ a = 1 := coe_eq_coe
Equivalence of Injected Element and One in $\text{WithTop}\ \alpha$
Informal description
For any element $a$ in $\alpha$, the injection of $a$ into $\text{WithTop}\ \alpha$ equals the one element of $\text{WithTop}\ \alpha$ if and only if $a$ equals the one element of $\alpha$. In symbols, $(a : \text{WithTop}\ \alpha) = 1 \leftrightarrow a = 1$.
WithTop.one_eq_coe theorem
: 1 = (a : WithTop α) ↔ a = 1
Full source 
@[to_additive (attr := simp, norm_cast)]
lemma one_eq_coe : 1 = (a : WithTop α) ↔ a = 1 := eq_comm.trans coe_eq_one
Equivalence of One and Injected Element in $\text{WithTop}\ \alpha$
Informal description
For any element $a$ of a type $\alpha$ with a one element, the equality $1 = (a : \text{WithTop}\ \alpha)$ holds if and only if $a = 1$ in $\alpha$.
WithTop.top_ne_one theorem
: (⊤ : WithTop α) ≠ 1
Full source 
@[to_additive (attr := simp)] lemma top_ne_one : (⊤ : WithTop α) ≠ 1 := top_ne_coe
Top element is not equal to one in `WithTop α`
Informal description
In the type `WithTop α` (the type `α` extended with a top element `⊤`), the top element is not equal to the one element, i.e., $\top \neq 1$.
WithTop.one_ne_top theorem
: (1 : WithTop α) ≠ ⊤
Full source 
@[to_additive (attr := simp)] lemma one_ne_top : (1 : WithTop α) ≠ ⊤ := coe_ne_top
Inequality between One and Top in $\text{WithTop}\ \alpha$
Informal description
In the type $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$), the one element is not equal to the top element, i.e., $1 \neq \top$.
WithTop.untop_one theorem
: (1 : WithTop α).untop coe_ne_top = 1
Full source 
@[to_additive (attr := simp)]
theorem untop_one : (1 : WithTop α).untop coe_ne_top = 1 :=
  rfl
Underlying element of one in `WithTop α` is one
Informal description
For the type `WithTop α` (the type `α` extended with a top element `⊤`), the underlying element of the one element `1` (when viewed as an element of `WithTop α`) is equal to `1` in `α`. That is, if we extract the underlying element from `1 : WithTop α` (which is guaranteed to not be `⊤`), we get `1 : α`.
WithTop.untopD_one theorem
(d : α) : (1 : WithTop α).untopD d = 1
Full source 
@[to_additive (attr := simp)]
theorem untopD_one (d : α) : (1 : WithTop α).untopD d = 1 :=
  rfl
Default Extraction of One in $\text{WithTop}\ \alpha$ Yields One
Informal description
For any default value $d$ in a type $\alpha$, extracting the underlying value of the element $1$ in $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$) with the default $d$ yields $1$ in $\alpha$. That is, $(1 : \text{WithTop}\ \alpha).\text{untopD}\ d = 1$.
WithTop.one_le_coe theorem
[LE α] {a : α} : 1 ≤ (a : WithTop α) ↔ 1 ≤ a
Full source 
@[to_additive (attr := simp, norm_cast) coe_nonneg]
theorem one_le_coe [LE α] {a : α} : 1 ≤ (a : WithTop α) ↔ 1 ≤ a :=
  coe_le_coe
Order Preservation of One in Type Extended with Top Element
Informal description
For any element $a$ of a type $\alpha$ with a partial order, the inequality $1 \leq a$ holds in $\alpha$ extended with a top element (denoted as $\alpha \cup \{\top\}$) if and only if $1 \leq a$ holds in $\alpha$.
WithTop.coe_le_one theorem
[LE α] {a : α} : (a : WithTop α) ≤ 1 ↔ a ≤ 1
Full source 
@[to_additive (attr := simp, norm_cast) coe_le_zero]
theorem coe_le_one [LE α] {a : α} : (a : WithTop α) ≤ 1 ↔ a ≤ 1 :=
  coe_le_coe
Order Preservation of One in $\text{WithTop}\ \alpha$
Informal description
For any element $a$ of a type $\alpha$ equipped with a partial order, the inequality $(a : \text{WithTop}\ \alpha) \leq 1$ holds if and only if $a \leq 1$ holds in $\alpha$.
WithTop.one_lt_coe theorem
[LT α] {a : α} : 1 < (a : WithTop α) ↔ 1 < a
Full source 
@[to_additive (attr := simp, norm_cast) coe_pos]
theorem one_lt_coe [LT α] {a : α} : 1 < (a : WithTop α) ↔ 1 < a :=
  coe_lt_coe
Preservation of $1 < a$ in $\text{WithTop}\ \alpha$
Informal description
For any element $a$ of a type $\alpha$ with a strict order, the inequality $1 < a$ holds in $\alpha$ extended with a top element (denoted as $\text{WithTop}\ \alpha$) if and only if $1 < a$ holds in $\alpha$.
WithTop.coe_lt_one theorem
[LT α] {a : α} : (a : WithTop α) < 1 ↔ a < 1
Full source 
@[to_additive (attr := simp, norm_cast) coe_lt_zero]
theorem coe_lt_one [LT α] {a : α} : (a : WithTop α) < 1 ↔ a < 1 :=
  coe_lt_coe
Inequality Preservation of One in $\text{WithTop}\ \alpha$
Informal description
For any element $a$ of type $\alpha$ with a strict order, the inequality $a < 1$ holds in $\text{WithTop}\ \alpha$ if and only if $a < 1$ holds in $\alpha$.
WithTop.map_one theorem
{β} (f : α → β) : (1 : WithTop α).map f = (f 1 : WithTop β)
Full source 
@[to_additive (attr := simp)]
protected theorem map_one {β} (f : α → β) : (1 : WithTop α).map f = (f 1 : WithTop β) :=
  rfl
Lifted Map Preserves Multiplicative Identity in $\text{WithTop}$
Informal description
For any function $f : \alpha \to \beta$, the image of the multiplicative identity $1$ in $\text{WithTop}\ \alpha$ under the lifted map $\text{WithTop.map}\ f$ is equal to the image of $1$ under $f$ in $\text{WithTop}\ \beta$, i.e., $\text{WithTop.map}\ f\ 1 = f(1)$.
WithTop.map_eq_one_iff theorem
{α} {f : α → β} {v : WithTop α} [One β] : WithTop.map f v = 1 ↔ ∃ x, v = .some x ∧ f x = 1
Full source 
@[to_additive]
theorem map_eq_one_iff {α} {f : α → β} {v : WithTop α} [One β] :
    WithTop.mapWithTop.map f v = 1 ↔ ∃ x, v = .some x ∧ f x = 1 := map_eq_some_iff
Characterization of Lifted Map Output as One in $\text{WithTop}\ \alpha$
Informal description
For a function $f : \alpha \to \beta$ and an element $v \in \text{WithTop}\ \alpha$, the lifted map $\text{WithTop.map}\ f$ applied to $v$ equals the multiplicative identity $1$ of $\beta$ if and only if there exists an element $x \in \alpha$ such that $v = x$ (viewed in $\text{WithTop}\ \alpha$) and $f(x) = 1$.
WithTop.one_eq_map_iff theorem
{α} {f : α → β} {v : WithTop α} [One β] : 1 = WithTop.map f v ↔ ∃ x, v = .some x ∧ f x = 1
Full source 
@[to_additive]
theorem one_eq_map_iff {α} {f : α → β} {v : WithTop α} [One β] :
    1 = WithTop.map f v ↔ ∃ x, v = .some x ∧ f x = 1 := some_eq_map_iff
Characterization of Preimage of One under Lifted Map in $\text{WithTop}$
Informal description
For any function $f : \alpha \to \beta$ and element $v \in \text{WithTop}\ \alpha$, the equality $1 = \text{WithTop.map}\ f\ v$ holds if and only if there exists an element $x \in \alpha$ such that $v = \text{some}\ x$ and $f(x) = 1$.
WithTop.zeroLEOneClass instance
[Zero α] [LE α] [ZeroLEOneClass α] : ZeroLEOneClass (WithTop α)
Full source 
instance zeroLEOneClass [Zero α] [LE α] [ZeroLEOneClass α] : ZeroLEOneClass (WithTop α) :=
  ⟨coe_le_coe.2 zero_le_one⟩
Preservation of $0 \leq 1$ in $\text{WithTop}\ \alpha$
Informal description
For any type $\alpha$ with a zero element $0$, a one element $1$, a less-or-equal relation $\leq$, and satisfying $0 \leq 1$, the type $\text{WithTop}\ \alpha$ (obtained by adjoining a top element to $\alpha$) also satisfies $0 \leq 1$.
WithTop.add instance
: Add (WithTop α)
Full source 
instance add : Add (WithTop α) :=
  ⟨Option.map₂ (· + ·)⟩
Addition on Type Extended with a Top Element
Informal description
The type `WithTop α`, which extends a type `α` by adding a top element `⊤`, can be equipped with an addition operation that extends the addition on `α`. The addition is defined such that adding any element to `⊤` results in `⊤`.
WithTop.coe_add theorem
(a b : α) : ↑(a + b) = (a + b : WithTop α)
Full source 
@[simp, norm_cast] lemma coe_add (a b : α) : ↑(a + b) = (a + b : WithTop α) := rfl
Injection Preserves Addition in $\text{WithTop}\ \alpha$
Informal description
For any elements $a, b$ in a type $\alpha$, the canonical injection of their sum $a + b$ into $\text{WithTop}\ \alpha$ is equal to the sum of their injections, i.e., $\uparrow(a + b) = \uparrow a + \uparrow b$ in $\text{WithTop}\ \alpha$.
WithTop.top_add theorem
(x : WithTop α) : ⊤ + x = ⊤
Full source 
@[simp] lemma top_add (x : WithTop α) : ⊤ + x = ⊤ := rfl
Top Element Absorbs Addition in $\text{WithTop}\ \alpha$
Informal description
For any element $x$ in the type $\alpha$ extended with a top element $\top$, the sum $\top + x$ equals $\top$.
WithTop.add_top theorem
(x : WithTop α) : x + ⊤ = ⊤
Full source 
@[simp] lemma add_top (x : WithTop α) : x + ⊤ = ⊤ := by cases x <;> rfl
Top Element Absorbs Addition from the Right in $\text{WithTop}\ \alpha$
Informal description
For any element $x$ in the type $\alpha$ extended with a top element $\top$, the sum $x + \top$ equals $\top$.
WithTop.add_eq_top theorem
: x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
Full source 
@[simp] lemma add_eq_top : x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤ := by cases x <;> cases y <;> simp [← coe_add]
Sum Equals Top iff Either Summand is Top in $\text{WithTop}\ \alpha$
Informal description
For any elements $x$ and $y$ in the type $\alpha$ extended with a top element $\top$, the sum $x + y$ equals $\top$ if and only if either $x = \top$ or $y = \top$.
WithTop.add_ne_top theorem
: x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
Full source 
lemma add_ne_top : x + y ≠ ⊤x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤ := by cases x <;> cases y <;> simp [← coe_add]
Sum Not Equal to Top in Extended Type if and only if Neither Summand is Top
Informal description
For any elements $x$ and $y$ in the type $\alpha$ extended with a top element $\top$, the sum $x + y$ is not equal to $\top$ if and only if neither $x$ nor $y$ is equal to $\top$.
WithTop.add_lt_top theorem
[LT α] : x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
Full source 
@[simp]
lemma add_lt_top [LT α] : x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤ := by
  simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]
Sum Strictly Below Top in Extended Ordered Type
Informal description
For any type $\alpha$ with a strict order and elements $x, y$ in $\alpha$ extended with a top element $\top$, the sum $x + y$ is strictly less than $\top$ if and only if both $x$ and $y$ are strictly less than $\top$.
WithTop.add_eq_coe theorem
: ∀ {a b : WithTop α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
Full source 
theorem add_eq_coe :
    ∀ {a b : WithTop α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
  | ⊤, b, c => by simp
  | some a, ⊤, c => by simp
  | some a, some b, c => by norm_cast; simp
Sum Equals Lifted Element in Extended Type if and only if Sum of Preimages Exists
Informal description
For any elements $a, b$ in the type $\alpha$ extended with a top element $\top$ and any element $c \in \alpha$, the sum $a + b$ equals $c$ if and only if there exist elements $a', b' \in \alpha$ such that $a'$ is the image of $a$ under the canonical injection, $b'$ is the image of $b$ under the canonical injection, and $a' + b' = c$ in $\alpha$.
WithTop.add_coe_eq_top_iff theorem
: x + b = ⊤ ↔ x = ⊤
Full source 
lemma add_coe_eq_top_iff : x + b = ⊤ ↔ x = ⊤ := by simp
Sum Equals Top in Extended Type if and only if First Summand is Top
Informal description
For any element $x$ in $\text{WithTop}\ \alpha$ and any element $b$ in $\alpha$, the sum $x + b$ equals the top element $\top$ if and only if $x$ equals $\top$.
WithTop.coe_add_eq_top_iff theorem
: a + y = ⊤ ↔ y = ⊤
Full source 
lemma coe_add_eq_top_iff : a + y = ⊤ ↔ y = ⊤ := by simp
Sum Equals Top in $\text{WithTop}\ \alpha$ if and only if Second Summand is Top
Informal description
For any element $a$ in $\text{WithTop}\ \alpha$ and any element $y$ in $\alpha$, the sum $a + y$ equals the top element $\top$ if and only if $y$ equals $\top$.
WithTop.add_right_inj theorem
[IsRightCancelAdd α] (hz : z ≠ ⊤) : x + z = y + z ↔ x = y
Full source 
lemma add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊤) : x + z = y + z ↔ x = y := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]
Right Cancellation Law for Addition in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type with a right cancellative addition operation, and let $x, y, z$ be elements of $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$). If $z \neq \top$, then the equation $x + z = y + z$ holds if and only if $x = y$.
WithTop.add_right_cancel theorem
[IsRightCancelAdd α] (hz : z ≠ ⊤) (h : x + z = y + z) : x = y
Full source 
lemma add_right_cancel [IsRightCancelAdd α] (hz : z ≠ ⊤) (h : x + z = y + z) : x = y :=
  (WithTop.add_right_inj hz).1 h
Right Cancellation of Addition in $\text{WithTop}\ \alpha$ for Non-Top Elements
Informal description
Let $\alpha$ be a type with a right cancellative addition operation, and let $x, y, z$ be elements of $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$). If $z \neq \top$ and $x + z = y + z$, then $x = y$.
WithTop.add_left_inj theorem
[IsLeftCancelAdd α] (hx : x ≠ ⊤) : x + y = x + z ↔ y = z
Full source 
lemma add_left_inj [IsLeftCancelAdd α] (hx : x ≠ ⊤) : x + y = x + z ↔ y = z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]
Left Cancellation of Addition in $\text{WithTop}\ \alpha$ for Non-Top Elements
Informal description
Let $\alpha$ be a type with a left-cancellative addition operation, and let $x, y, z$ be elements of $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$). If $x \neq \top$, then the equality $x + y = x + z$ holds if and only if $y = z$.
WithTop.add_left_cancel theorem
[IsLeftCancelAdd α] (hx : x ≠ ⊤) (h : x + y = x + z) : y = z
Full source 
lemma add_left_cancel [IsLeftCancelAdd α] (hx : x ≠ ⊤) (h : x + y = x + z) : y = z :=
  (WithTop.add_left_inj hx).1 h
Left cancellation of addition in $\text{WithTop}\ \alpha$ for non-top elements
Informal description
Let $\alpha$ be a type with a left-cancellative addition operation, and let $x, y, z$ be elements of $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$). If $x \neq \top$ and $x + y = x + z$, then $y = z$.
WithTop.addLeftMono instance
[LE α] [AddLeftMono α] : AddLeftMono (WithTop α)
Full source 
instance addLeftMono [LE α] [AddLeftMono α] : AddLeftMono (WithTop α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using (add_le_add_left · _)
Left-Monotonicity of Addition in $\text{WithTop}\ \alpha$
Informal description
For any type $\alpha$ with a partial order $\leq$ and an addition operation that is left-monotonic (i.e., $b_1 \leq b_2$ implies $a + b_1 \leq a + b_2$ for all $a, b_1, b_2 \in \alpha$), the type $\alpha$ extended with a top element $\top$ also has a left-monotonic addition operation.
WithTop.addRightMono instance
[LE α] [AddRightMono α] : AddRightMono (WithTop α)
Full source 
instance addRightMono [LE α] [AddRightMono α] : AddRightMono (WithTop α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using (add_le_add_right · _)
Right-Monotonicity of Addition in $\text{WithTop}\ \alpha$
Informal description
For any type $\alpha$ with a partial order $\leq$ and an addition operation that is right-monotonic (i.e., $a_1 \leq a_2$ implies $a_1 + b \leq a_2 + b$ for all $a_1, a_2, b \in \alpha$), the type $\alpha$ extended with a top element $\top$ also has a right-monotonic addition operation.
WithTop.addLeftReflectLT instance
[LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithTop α)
Full source 
instance addLeftReflectLT [LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithTop α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_left
Addition Reflects Strict Order from the Left in $\alpha$ Extended with $\top$
Informal description
For any type $\alpha$ with a strict order relation $<$ and an addition operation that reflects the strict order from the left (i.e., $a + b_1 < a + b_2$ implies $b_1 < b_2$ for all $a, b_1, b_2 \in \alpha$), the type $\alpha$ extended with a top element $\top$ also satisfies the property that addition reflects the strict order from the left.
WithTop.addRightReflectLT instance
[LT α] [AddRightReflectLT α] : AddRightReflectLT (WithTop α)
Full source 
instance addRightReflectLT [LT α] [AddRightReflectLT α] : AddRightReflectLT (WithTop α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_right
Addition Reflects Strict Order from the Right in $\alpha$ Extended with $\top$
Informal description
For any type $\alpha$ with a strict order relation $<$ and an addition operation that reflects the strict order from the right (i.e., $a_1 + b < a_2 + b$ implies $a_1 < a_2$ for all $a_1, a_2, b \in \alpha$), the type $\alpha$ extended with a top element $\top$ also satisfies the property that addition reflects the strict order from the right.
WithTop.le_of_add_le_add_left theorem
[LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : x + y ≤ x + z → y ≤ z
Full source 
protected lemma le_of_add_le_add_left [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
    x + y ≤ x + z → y ≤ z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using le_of_add_le_add_left
Left Cancellation of Addition in $\text{WithTop}\ \alpha$ Preserves Order
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation that reflects the order from the left (i.e., for all $a, b_1, b_2 \in \alpha$, $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$). For any elements $x, y, z$ in $\alpha$ extended with a top element $\top$, if $x \neq \top$ and $x + y \leq x + z$, then $y \leq z$.
WithTop.le_of_add_le_add_right theorem
[LE α] [AddRightReflectLE α] (hz : z ≠ ⊤) : x + z ≤ y + z → x ≤ y
Full source 
protected lemma le_of_add_le_add_right [LE α] [AddRightReflectLE α] (hz : z ≠ ⊤) :
    x + z ≤ y + z → x ≤ y := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using le_of_add_le_add_right
Right Addition Reflects Order in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation that reflects the order from the right (i.e., $a_1 + b \leq a_2 + b$ implies $a_1 \leq a_2$ for all $a_1, a_2, b \in \alpha$). For any elements $x, y, z$ in $\alpha$ extended with a top element $\top$, if $z \neq \top$ and $x + z \leq y + z$, then $x \leq y$.
WithTop.add_lt_add_left theorem
[LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) : y < z → x + y < x + z
Full source 
protected lemma add_lt_add_left [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) :
    y < z → x + y < x + z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using (add_lt_add_left · _)
Strict Left Monotonicity of Addition in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type with a strict order $<$ and an addition operation $+$ such that addition on the left is strictly monotone. For any $x, y, z \in \text{WithTop}\ \alpha$ with $x \neq \top$, if $y < z$, then $x + y < x + z$.
WithTop.add_lt_add_right theorem
[LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) : x < y → x + z < y + z
Full source 
protected lemma add_lt_add_right [LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) :
    x < y → x + z < y + z := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using (add_lt_add_right · _)
Right Addition Preserves Strict Inequality in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type with a strict order $<$ and a right-strictly monotone addition operation $+$. For any elements $x, y, z \in \text{WithTop}\ \alpha$ such that $z \neq \top$, if $x < y$, then $x + z < y + z$.
WithTop.add_le_add_iff_left theorem
[LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : x + y ≤ x + z ↔ y ≤ z
Full source 
protected lemma add_le_add_iff_left [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
    x + y ≤ x + z ↔ y ≤ z := ⟨WithTop.le_of_add_le_add_left hx, (add_le_add_left · _)⟩
Left Cancellation of Addition in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation that is left-monotonic and reflects the order from the left. For any elements $x, y, z$ in $\alpha$ extended with a top element $\top$, if $x \neq \top$, then $x + y \leq x + z$ if and only if $y \leq z$.
WithTop.add_le_add_iff_right theorem
[LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊤) : x + z ≤ y + z ↔ x ≤ y
Full source 
protected lemma add_le_add_iff_right [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊤) :
    x + z ≤ y + z ↔ x ≤ y := ⟨WithTop.le_of_add_le_add_right hz, (add_le_add_right · _)⟩
Right Addition Preserves and Reflects Order in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation that is right-monotonic (i.e., $a_1 \leq a_2$ implies $a_1 + b \leq a_2 + b$ for all $a_1, a_2, b \in \alpha$) and reflects the order from the right (i.e., $a_1 + b \leq a_2 + b$ implies $a_1 \leq a_2$ for all $a_1, a_2, b \in \alpha$). For any elements $x, y, z$ in $\alpha$ extended with a top element $\top$, if $z \neq \top$, then $x + z \leq y + z$ if and only if $x \leq y$.
WithTop.add_lt_add_iff_left theorem
[LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊤) : x + y < x + z ↔ y < z
Full source 
protected lemma add_lt_add_iff_left [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊤) :
    x + y < x + z ↔ y < z := ⟨lt_of_add_lt_add_left, WithTop.add_lt_add_left hx⟩
Left Addition Preserves Strict Order in $\text{WithTop}\ \alpha$: $x + y < x + z \leftrightarrow y < z$ for $x \neq \top$
Informal description
Let $\alpha$ be a type with a strict order $<$ and an addition operation $+$ such that addition on the left is strictly monotone and reflects the strict order. For any $x, y, z \in \text{WithTop}\ \alpha$ with $x \neq \top$, the inequality $x + y < x + z$ holds if and only if $y < z$.
WithTop.add_lt_add_iff_right theorem
[LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ≠ ⊤) : x + z < y + z ↔ x < y
Full source 
protected lemma add_lt_add_iff_right [LT α] [AddRightStrictMono α] [AddRightReflectLT α]
    (hz : z ≠ ⊤) : x + z < y + z ↔ x < y := ⟨lt_of_add_lt_add_right, WithTop.add_lt_add_right hz⟩
Right Addition Preserves and Reflects Strict Inequality in $\alpha$ Extended with $\top$
Informal description
Let $\alpha$ be a type with a strict order $<$ and an addition operation that is right-strictly monotone and reflects the strict order from the right. For any elements $x, y, z \in \alpha$ extended with a top element $\top$ (where $z \neq \top$), the inequality $x + z < y + z$ holds if and only if $x < y$.
WithTop.add_lt_add_of_le_of_lt theorem
[Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊤) (hwy : w ≤ y) (hxz : x < z) : w + x < y + z
Full source 
protected theorem add_lt_add_of_le_of_lt [Preorder α] [AddLeftStrictMono α]
    [AddRightMono α] (hw : w ≠ ⊤) (hwy : w ≤ y) (hxz : x < z) :
    w + x < y + z :=
  (WithTop.add_lt_add_left hw hxz).trans_le <| add_le_add_right hwy _
Strict Inequality Preservation Under Addition in $\text{WithTop}\ \alpha$ with Mixed Bounds
Informal description
Let $\alpha$ be a type with a preorder $\leq$ and an addition operation $+$ such that: 1. Addition on the left is strictly monotone (i.e., $b_1 < b_2$ implies $a + b_1 < a + b_2$ for all $a, b_1, b_2 \in \alpha$) 2. Addition on the right is monotone (i.e., $a_1 \leq a_2$ implies $a_1 + b \leq a_2 + b$ for all $a_1, a_2, b \in \alpha$) For any elements $w, x, y, z \in \text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$) where: - $w \neq \top$ - $w \leq y$ - $x < z$ it follows that $w + x < y + z$.
WithTop.add_lt_add_of_lt_of_le theorem
[Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊤) (hwy : w < y) (hxz : x ≤ z) : w + x < y + z
Full source 
protected theorem add_lt_add_of_lt_of_le [Preorder α] [AddLeftMono α]
    [AddRightStrictMono α] (hx : x ≠ ⊤) (hwy : w < y) (hxz : x ≤ z) :
    w + x < y + z :=
  (WithTop.add_lt_add_right hx hwy).trans_le <| add_le_add_left hxz _
Strict Inequality Preservation under Addition in $\text{WithTop}\ \alpha$ with Mixed Conditions
Informal description
Let $\alpha$ be a type with a preorder $\leq$ and addition operations that are left-monotonic and right-strictly monotonic. For elements $w, x, y, z \in \text{WithTop}\ \alpha$ such that $x \neq \top$, if $w < y$ and $x \leq z$, then $w + x < y + z$.
WithTop.addLECancellable_of_ne_top theorem
[LE α] [ContravariantClass α α (· + ·) (· ≤ ·)] (hx : x ≠ ⊤) : AddLECancellable x
Full source 
lemma addLECancellable_of_ne_top [LE α] [ContravariantClass α α (· + ·) (· ≤ ·)]
    (hx : x ≠ ⊤) : AddLECancellable x := fun _b _c ↦ WithTop.le_of_add_le_add_left hx
Additive Left Cancellation in $\text{WithTop}\ \alpha$ for Non-Top Elements
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation such that for all $a, b, c \in \alpha$, $a + b \leq a + c$ implies $b \leq c$. For any element $x$ in $\alpha$ extended with a top element $\top$, if $x \neq \top$, then $x$ is additively left cancellable with respect to $\leq$, i.e., for all $y, z \in \text{WithTop}\ \alpha$, $x + y \leq x + z$ implies $y \leq z$.
WithTop.addLECancellable_of_lt_top theorem
[Preorder α] [ContravariantClass α α (· + ·) (· ≤ ·)] (hx : x < ⊤) : AddLECancellable x
Full source 
lemma addLECancellable_of_lt_top [Preorder α] [ContravariantClass α α (· + ·) (· ≤ ·)]
    (hx : x < ⊤) : AddLECancellable x := addLECancellable_of_ne_top hx.ne
Additive Left Cancellation in $\text{WithTop}\ \alpha$ for Elements Below Top
Informal description
Let $\alpha$ be a type with a preorder $\leq$ and an addition operation such that for all $a, b, c \in \alpha$, $a + b \leq a + c$ implies $b \leq c$. For any element $x$ in $\alpha$ extended with a top element $\top$, if $x < \top$, then $x$ is additively left cancellable with respect to $\leq$, i.e., for all $y, z \in \text{WithTop}\ \alpha$, $x + y \leq x + z$ implies $y \leq z$.
WithTop.addLECancellable_coe theorem
[LE α] [ContravariantClass α α (· + ·) (· ≤ ·)] (a : α) : AddLECancellable (a : WithTop α)
Full source 
lemma addLECancellable_coe [LE α] [ContravariantClass α α (· + ·) (· ≤ ·)] (a : α) :
    AddLECancellable (a : WithTop α) := addLECancellable_of_ne_top coe_ne_top
Additive Left Cancellation for Embedded Elements in $\text{WithTop}\ \alpha$
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation such that for all $a, b, c \in \alpha$, $a + b \leq a + c$ implies $b \leq c$. For any element $a \in \alpha$, the canonical embedding of $a$ into $\text{WithTop}\ \alpha$ is additively left cancellable with respect to $\leq$, i.e., for all $y, z \in \text{WithTop}\ \alpha$, $a + y \leq a + z$ implies $y \leq z$.
WithTop.addLECancellable_iff_ne_top theorem
[Nonempty α] [Preorder α] [ContravariantClass α α (· + ·) (· ≤ ·)] : AddLECancellable x ↔ x ≠ ⊤
Full source 
lemma addLECancellable_iff_ne_top [Nonempty α] [Preorder α]
    [ContravariantClass α α (· + ·) (· ≤ ·)] : AddLECancellableAddLECancellable x ↔ x ≠ ⊤ where
  mp := by rintro h rfl; exact (coe_lt_top <| Classical.arbitrary _).not_le <| h <| by simp
  mpr := addLECancellable_of_ne_top
Additive Left Cancellation in $\alpha \cup \{\top\}$ is Equivalent to Not Being the Top Element
Informal description
Let $\alpha$ be a nonempty type equipped with a preorder and an addition operation such that for all $a, b, c \in \alpha$, $a + b \leq a + c$ implies $b \leq c$. For any element $x$ in $\alpha$ extended with a top element $\top$, $x$ is additively left cancellable with respect to $\leq$ if and only if $x \neq \top$.
WithTop.map_add theorem
{F} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithTop α) : (a + b).map f = a.map f + b.map f
Full source 
@[simp]
protected theorem map_add {F} [Add β] [FunLike F α β] [AddHomClass F α β]
    (f : F) (a b : WithTop α) :
    (a + b).map f = a.map f + b.map f := by
  induction a
  · exact (top_add _).symm
  · induction b
    · exact (add_top _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl
Homomorphism Property of Map over Addition in $\alpha \cup \{\top\}$
Informal description
Let $\alpha$ and $\beta$ be types with addition operations, and let $F$ be a type of addition-preserving homomorphisms from $\alpha$ to $\beta$. For any $f \in F$ and any elements $a, b$ in $\alpha$ extended with a top element $\top$, the map $f$ applied to the sum $a + b$ equals the sum of $f$ applied to $a$ and $f$ applied to $b$, i.e., $$(a + b).\text{map}\, f = a.\text{map}\, f + b.\text{map}\, f.$$
WithTop.addSemigroup instance
[AddSemigroup α] : AddSemigroup (WithTop α)
Full source 
instance addSemigroup [AddSemigroup α] : AddSemigroup (WithTop α) :=
  { WithTop.add with
    add_assoc := fun _ _ _ => Option.map₂_assoc add_assoc }
Additive Semigroup Structure on $\alpha \cup \{\top\}$
Informal description
For any additive semigroup $\alpha$, the type $\alpha$ extended with a top element $\top$ forms an additive semigroup, where addition is defined by extending the addition on $\alpha$ and setting $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$.
WithTop.addCommSemigroup instance
[AddCommSemigroup α] : AddCommSemigroup (WithTop α)
Full source 
instance addCommSemigroup [AddCommSemigroup α] : AddCommSemigroup (WithTop α) :=
  { WithTop.addSemigroup with
    add_comm := fun _ _ => Option.map₂_comm add_comm }
Additive Commutative Semigroup Structure on $\alpha \cup \{\top\}$
Informal description
For any additive commutative semigroup $\alpha$, the type $\alpha$ extended with a top element $\top$ forms an additive commutative semigroup, where addition is defined by extending the commutative addition on $\alpha$ and setting $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$.
WithTop.addZeroClass instance
[AddZeroClass α] : AddZeroClass (WithTop α)
Full source 
instance addZeroClass [AddZeroClass α] : AddZeroClass (WithTop α) :=
  { WithTop.zero, WithTop.add with
    zero_add := Option.map₂_left_identity zero_add
    add_zero := Option.map₂_right_identity add_zero }
Additive Zero Class Structure on $\alpha \cup \{\top\}$
Informal description
For any type $\alpha$ equipped with an addition operation and a zero element satisfying the additive identity laws, the type $\alpha$ extended with a top element $\top$ also forms an additive zero class. The addition is extended such that $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$, and the zero element is preserved.
WithTop.addMonoid instance
: AddMonoid (WithTop α)
Full source 
instance addMonoid : AddMonoid (WithTop α) where
  __ := WithTop.addSemigroup
  __ := WithTop.addZeroClass
  nsmul n a := match a, n with
    | (a : α), n => ↑(n • a)
    | ⊤, 0 => 0
    | ⊤, _n + 1 => ⊤
  nsmul_zero a := by cases a <;> simp [zero_nsmul]
  nsmul_succ n a := by cases a <;> cases n <;> simp [succ_nsmul, coe_add]
Additive Monoid Structure on $\alpha \cup \{\top\}$
Informal description
For any additive monoid $\alpha$, the type $\alpha$ extended with a top element $\top$ forms an additive monoid, where addition is defined by extending the addition on $\alpha$ and setting $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$, and the zero element is preserved.
WithTop.coe_nsmul theorem
(a : α) (n : ℕ) : ↑(n • a) = n • (a : WithTop α)
Full source 
@[simp, norm_cast] lemma coe_nsmul (a : α) (n : ℕ) : ↑(n • a) = n • (a : WithTop α) := rfl
Preservation of Scalar Multiplication in $\alpha \cup \{\top\}$
Informal description
For any element $a$ of an additive monoid $\alpha$ and any natural number $n$, the scalar multiplication $n \cdot a$ in $\alpha$ is preserved when lifted to $\text{WithTop}\ \alpha$, i.e., $\uparrow(n \cdot a) = n \cdot \uparrow a$.
WithTop.addHom definition
: α →+ WithTop α
Full source 
/-- Coercion from `α` to `WithTop α` as an `AddMonoidHom`. -/
def addHom : α →+ WithTop α where
  toFun := WithTop.some
  map_zero' := rfl
  map_add' _ _ := rfl
Inclusion homomorphism from $\alpha$ to $\alpha \cup \{\top\}$
Informal description
The additive monoid homomorphism that injects an element of type $\alpha$ into $\text{WithTop}\ \alpha$ by mapping $a \in \alpha$ to $\text{some}\ a \in \text{WithTop}\ \alpha$. This homomorphism preserves the zero element and addition, i.e., it satisfies: 1. $f(0) = 0$ 2. $f(x + y) = f(x) + f(y)$ for all $x, y \in \alpha$
WithTop.coe_addHom theorem
: ⇑(addHom : α →+ WithTop α) = WithTop.some
Full source 
@[simp, norm_cast] lemma coe_addHom : ⇑(addHom : α →+ WithTop α) = WithTop.some := rfl
Underlying Function of Inclusion Homomorphism Equals Canonical Injection
Informal description
The underlying function of the additive monoid homomorphism `addHom` from $\alpha$ to $\text{WithTop}\ \alpha$ is equal to the canonical injection $\text{some} : \alpha \to \text{WithTop}\ \alpha$.
WithTop.addCommMonoid instance
[AddCommMonoid α] : AddCommMonoid (WithTop α)
Full source 
instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (WithTop α) :=
  { WithTop.addMonoid, WithTop.addCommSemigroup with }
Additive Commutative Monoid Structure on $\alpha \cup \{\top\}$
Informal description
For any additive commutative monoid $\alpha$, the type $\alpha$ extended with a top element $\top$ forms an additive commutative monoid, where addition is defined by extending the commutative addition on $\alpha$ and setting $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$.
WithTop.addMonoidWithOne instance
: AddMonoidWithOne (WithTop α)
Full source 
instance addMonoidWithOne : AddMonoidWithOne (WithTop α) :=
  { WithTop.one, WithTop.addMonoid with
    natCast := fun n => ↑(n : α),
    natCast_zero := by
      simp only [Nat.cast_zero, WithTop.coe_zero],
    natCast_succ := fun n => by
      simp only [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one] }
Additive Monoid with One Structure on $\alpha \cup \{\top\}$
Informal description
For any additive monoid with one $\alpha$, the type $\alpha$ extended with a top element $\top$ forms an additive monoid with one, where addition and the one element are defined by extending the operations from $\alpha$ and setting $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$, and the one element is preserved.
WithTop.coe_natCast theorem
(n : ℕ) : ((n : α) : WithTop α) = n
Full source 
@[simp, norm_cast] lemma coe_natCast (n : ℕ) : ((n : α) : WithTop α) = n := rfl
Natural Number Coercion Preservation in $\alpha \cup \{\top\}$
Informal description
For any natural number $n$, the canonical injection of $n$ into $\alpha \cup \{\top\}$ (where $\alpha$ is an additive monoid with one) is equal to the natural number $n$ interpreted in $\alpha \cup \{\top\}$. In other words, the coercion map from $\alpha$ to $\alpha \cup \{\top\}$ preserves natural number constants.
WithTop.top_ne_natCast theorem
(n : ℕ) : (⊤ : WithTop α) ≠ n
Full source 
@[simp] lemma top_ne_natCast (n : ℕ) : (⊤ : WithTop α) ≠ n := top_ne_coe
Top Element is Distinct from Embedded Natural Numbers in $\alpha \cup \{\top\}$
Informal description
For any natural number $n$, the top element $\top$ in the type $\alpha$ extended with a top element is not equal to the canonical embedding of $n$ into $\text{WithTop}\ \alpha$.
WithTop.natCast_ne_top theorem
(n : ℕ) : (n : WithTop α) ≠ ⊤
Full source 
@[simp] lemma natCast_ne_top (n : ℕ) : (n : WithTop α) ≠ ⊤ := coe_ne_top
Natural Number Embedding is Not Top in Extended Type
Informal description
For any natural number $n$, the canonical embedding of $n$ into $\alpha \cup \{\top\}$ is not equal to the top element $\top$. In other words, $n \neq \top$ in $\text{WithTop}\ \alpha$.
WithTop.natCast_lt_top theorem
[LT α] (n : ℕ) : (n : WithTop α) < ⊤
Full source 
@[simp] lemma natCast_lt_top [LT α] (n : ℕ) : (n : WithTop α) < ⊤ := coe_lt_top _
Natural Numbers are Below Top in Extended Type
Informal description
For any natural number $n$ and any type $\alpha$ with a less-than relation, the injection of $n$ into $\alpha$ extended with a top element $\top$ is strictly less than $\top$, i.e., $n < \top$.
WithTop.coe_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : α) : WithTop α) = ofNat(n)
Full source 
@[simp] lemma coe_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : α) : WithTop α) = ofNat(n) := rfl
Commutativity of Natural Number Embedding in $\alpha \cup \{\top\}$ for $n \geq 2$
Informal description
For any natural number $n \geq 2$ and any type $\alpha$ with a canonical homomorphism from $\mathbb{N}$, the injection of the numeral $n$ into $\alpha$ followed by the embedding into $\alpha \cup \{\top\}$ equals the direct interpretation of $n$ in $\alpha \cup \{\top\}$. In other words, the following diagram commutes: $$ \text{ofNat}(n) : \alpha \hookrightarrow \text{WithTop}\ \alpha = \text{ofNat}(n) : \text{WithTop}\ \alpha $$
WithTop.coe_eq_ofNat theorem
(n : ℕ) [n.AtLeastTwo] (m : α) : (m : WithTop α) = ofNat(n) ↔ m = ofNat(n)
Full source 
@[simp] lemma coe_eq_ofNat (n : ℕ) [n.AtLeastTwo] (m : α) :
    (m : WithTop α) = ofNat(n) ↔ m = ofNat(n) :=
  coe_eq_coe
Equality of Injected Element and Numeric Literal in Extended Type: $(m : \alpha \cup \{\top\}) = n \leftrightarrow m = n$
Informal description
For any natural number $n \geq 2$ and any element $m$ of type $\alpha$, the injection of $m$ into $\alpha \cup \{\top\}$ equals the canonical interpretation of $n$ in $\alpha \cup \{\top\}$ if and only if $m$ equals the canonical interpretation of $n$ in $\alpha$.
WithTop.ofNat_eq_coe theorem
(n : ℕ) [n.AtLeastTwo] (m : α) : ofNat(n) = (m : WithTop α) ↔ ofNat(n) = m
Full source 
@[simp] lemma ofNat_eq_coe (n : ℕ) [n.AtLeastTwo] (m : α) :
    ofNat(n)ofNat(n) = (m : WithTop α) ↔ ofNat(n) = m :=
  coe_eq_coe
Equivalence of Numeral Equality in $\alpha \cup \{\top\}$
Informal description
For any natural number $n \geq 2$ and any element $m$ of type $\alpha$, the equality between the numeral $n$ and the injection of $m$ into $\alpha \cup \{\top\}$ holds if and only if $n$ equals $m$ in $\alpha$. That is, $n = (\text{some}\ m) \leftrightarrow n = m$.
WithTop.ofNat_ne_top theorem
(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : WithTop α) ≠ ⊤
Full source 
@[simp] lemma ofNat_ne_top (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : WithTop α) ≠ ⊤ :=
  natCast_ne_top n
Embedded Numerals Are Not Top in Extended Type
Informal description
For any natural number $n \geq 2$, the canonical embedding of $n$ into the type $\alpha$ extended with a top element $\top$ is not equal to $\top$. That is, $n \neq \top$ in $\alpha \cup \{\top\}$.
WithTop.top_ne_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : (⊤ : WithTop α) ≠ ofNat(n)
Full source 
@[simp] lemma top_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊤ : WithTop α) ≠ ofNat(n) :=
  top_ne_natCast n
Top Element is Distinct from Embedded Numerals ≥ 2 in $\alpha \cup \{\top\}$
Informal description
For any natural number $n \geq 2$, the top element $\top$ in the type $\alpha$ extended with a top element is not equal to the canonical embedding of $n$ into $\alpha \cup \{\top\}$.
WithTop.map_ofNat theorem
{f : α → β} (n : ℕ) [n.AtLeastTwo] : WithTop.map f (ofNat(n) : WithTop α) = f (ofNat(n))
Full source 
@[simp] lemma map_ofNat {f : α → β} (n : ℕ) [n.AtLeastTwo] :
    WithTop.map f (ofNat(n) : WithTop α) = f (ofNat(n)) := map_coe f n
Lifted Map Preserves Canonical Embedding of Numerals ≥ 2
Informal description
For any function $f \colon \alpha \to \beta$ and any natural number $n \geq 2$, the lifted map $\text{WithTop.map}\ f$ applied to the canonical embedding of $n$ in $\text{WithTop}\ \alpha$ equals $f$ applied to the canonical embedding of $n$ in $\alpha$. In other words, if $n$ is a natural number at least 2, then $\text{WithTop.map}\ f\ (n) = f(n)$.
WithTop.map_natCast theorem
{f : α → β} (n : ℕ) : WithTop.map f (n : WithTop α) = f n
Full source 
@[simp] lemma map_natCast {f : α → β} (n : ℕ) :
    WithTop.map f (n : WithTop α) = f n := map_coe f n
Lifted Map Preserves Natural Number Casting: $\text{WithTop.map}\ f(n) = f(n)$
Informal description
For any function $f : \alpha \to \beta$ and any natural number $n$, the lifted map $\text{WithTop.map}\ f$ applied to the natural number $n$ (viewed as an element of $\alpha \cup \{\top\}$) equals $f(n)$.
WithTop.map_eq_ofNat_iff theorem
{f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} : a.map f = ofNat(n) ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma map_eq_ofNat_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} :
    a.map f = ofNat(n) ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
Characterization of When Lifted Map Equals Canonical Embedding of $n \geq 2$
Informal description
For any function $f \colon \beta \to \alpha$, any natural number $n \geq 2$, and any element $a \in \beta \cup \{\top\}$, the lifted map $\text{WithTop.map}\ f$ applied to $a$ equals the canonical embedding of $n$ in $\alpha \cup \{\top\}$ if and only if there exists an element $x \in \beta$ such that $a = x$ and $f(x) = n$. In other words, $\text{WithTop.map}\ f(a) = n$ (where $n$ is viewed in $\text{WithTop}\ \alpha$) if and only if $a$ is of the form $\text{some}\ x$ for some $x \in \beta$ with $f(x) = n$.
WithTop.ofNat_eq_map_iff theorem
{f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} : ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma ofNat_eq_map_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithTop β} :
    ofNat(n)ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
Characterization of Preimage of Numerals under Lifted Map in $\alpha \cup \{\top\}$
Informal description
For any function $f : \beta \to \alpha$, any natural number $n \geq 2$, and any element $a \in \beta \cup \{\top\}$, the equality $n = \text{WithTop.map}\, f\, a$ holds if and only if there exists an element $x \in \beta$ such that $a = x$ and $f(x) = n$.
WithTop.map_eq_natCast_iff theorem
{f : β → α} {n : ℕ} {a : WithTop β} : a.map f = n ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma map_eq_natCast_iff {f : β → α} {n : ℕ} {a : WithTop β} :
    a.map f = n ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
Characterization of Lifted Map Output as Natural Number in $\alpha \cup \{\top\}$
Informal description
For any function $f : \beta \to \alpha$, natural number $n \in \mathbb{N}$, and element $a \in \text{WithTop}\ \beta$, the lifted map $\text{WithTop.map}\ f$ applied to $a$ equals $n$ if and only if there exists an element $x \in \beta$ such that $a = \text{some}\ x$ and $f(x) = n$.
WithTop.natCast_eq_map_iff theorem
{f : β → α} {n : ℕ} {a : WithTop β} : n = a.map f ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma natCast_eq_map_iff {f : β → α} {n : ℕ} {a : WithTop β} :
    n = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
Characterization of Natural Number Cast in Terms of Lifted Map
Informal description
For any function $f \colon \beta \to \alpha$, natural number $n \in \mathbb{N}$, and element $a \in \text{WithTop}\ \beta$, the equality $n = \text{map}\ f\ a$ holds if and only if there exists an element $x \in \beta$ such that $a = \text{some}\ x$ and $f(x) = n$.
WithTop.charZero instance
[AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α)
Full source 
instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α) :=
  { cast_injective := Function.Injective.comp (f := Nat.cast (R := α))
      (fun _ _ => WithTop.coe_eq_coe.1) Nat.cast_injective}
Characteristic Zero Preservation in $\alpha \cup \{\top\}$
Informal description
For any additive monoid with one $\alpha$ of characteristic zero, the type $\alpha$ extended with a top element $\top$ also has characteristic zero. This means the canonical map from natural numbers to $\text{WithTop}\ \alpha$ is injective.
WithTop.addCommMonoidWithOne instance
[AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α)
Full source 
instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α) :=
  { WithTop.addMonoidWithOne, WithTop.addCommMonoid with }
Additive Commutative Monoid with One Structure on $\alpha \cup \{\top\}$
Informal description
For any additive commutative monoid with one $\alpha$, the type $\alpha$ extended with a top element $\top$ forms an additive commutative monoid with one, where addition and the one element are defined by extending the operations from $\alpha$ and setting $\top + a = a + \top = \top$ for any $a \in \alpha \cup \{\top\}$.
WithTop.existsAddOfLE instance
[LE α] [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithTop α)
Full source 
instance existsAddOfLE [LE α] [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithTop α) :=
  ⟨fun {a} {b} =>
    match a, b with
    | ⊤, ⊤ => by simp
    | (a : α), ⊤ => fun _ => ⟨⊤, rfl⟩
    | (a : α), (b : α) => fun h => by
      obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)
      exact ⟨c, rfl⟩
    | ⊤, (b : α) => fun h => (not_top_le_coe _ h).elim⟩
Adjoining Top Preserves Existence of Additive Differences
Informal description
For any ordered additive monoid $\alpha$ with the property that for any elements $a \leq b$ there exists $c$ such that $a + c = b$, the type $\text{WithTop}\ \alpha$ (obtained by adjoining a top element to $\alpha$) also satisfies this property.
WithTop.one_lt_top theorem
[One α] [LT α] : (1 : WithTop α) < ⊤
Full source 
@[to_additive (attr := simp) top_pos]
theorem one_lt_top [One α] [LT α] : (1 : WithTop α) < ⊤ := coe_lt_top _
One is Less Than Top in $\text{WithTop}\ \alpha$
Informal description
For any type $\alpha$ with a distinguished element $1$ and a strict order relation $<$, the element $1$ in $\text{WithTop}\ \alpha$ is strictly less than the top element $\top$.
WithTop.zero_lt_coe theorem
[Zero α] [LT α] (a : α) : (0 : WithTop α) < a ↔ 0 < a
Full source 
@[norm_cast, deprecated coe_pos (since := "2024-10-22")]
theorem zero_lt_coe [Zero α] [LT α] (a : α) : (0 : WithTop α) < a ↔ 0 < a :=
  coe_lt_coe
Inequality Preservation of Zero in $\text{WithTop}\ \alpha$
Informal description
For any element $a$ of a type $\alpha$ with a zero element and a strict order, the inequality $0 < a$ holds in $\text{WithTop}\ \alpha$ if and only if $0 < a$ holds in $\alpha$.
OneHom.withTopMap definition
{M N : Type*} [One M] [One N] (f : OneHom M N) : OneHom (WithTop M) (WithTop N)
Full source 
/-- A version of `WithTop.map` for `OneHom`s. -/
@[to_additive (attr := simps -fullyApplied)
  "A version of `WithTop.map` for `ZeroHom`s"]
protected def _root_.OneHom.withTopMap {M N : Type*} [One M] [One N] (f : OneHom M N) :
    OneHom (WithTop M) (WithTop N) where
  toFun := WithTop.map f
  map_one' := by rw [WithTop.map_one, map_one, coe_one]
Lifting of identity-preserving homomorphism to `WithTop`
Informal description
Given types $M$ and $N$ each equipped with a distinguished element $1$, and a homomorphism $f : M \to N$ that preserves the identity element (i.e., $f(1) = 1$), the function `OneHom.withTopMap` lifts $f$ to a homomorphism between the types `WithTop M` and `WithTop N`. The lifted homomorphism applies $f$ to elements of $M$ and preserves the top element $\top$, while also preserving the identity element.
AddHom.withTopMap definition
{M N : Type*} [Add M] [Add N] (f : AddHom M N) : AddHom (WithTop M) (WithTop N)
Full source 
/-- A version of `WithTop.map` for `AddHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddHom.withTopMap {M N : Type*} [Add M] [Add N] (f : AddHom M N) :
    AddHom (WithTop M) (WithTop N) where
  toFun := WithTop.map f
  map_add' := WithTop.map_add f
Lifting of additive homomorphism to `WithTop`
Informal description
Given two types `M` and `N` equipped with addition operations, and a non-unital additive homomorphism `f : M → N`, the function `AddHom.withTopMap` lifts `f` to a non-unital additive homomorphism between the types `WithTop M` and `WithTop N`. The lifted homomorphism applies `f` to elements of `M` and preserves the top element `⊤`, while also preserving the addition operation.
AddMonoidHom.withTopMap definition
{M N : Type*} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : WithTop M →+ WithTop N
Full source 
/-- A version of `WithTop.map` for `AddMonoidHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddMonoidHom.withTopMap {M N : Type*} [AddZeroClass M] [AddZeroClass N]
    (f : M →+ N) : WithTopWithTop M →+ WithTop N :=
  { ZeroHom.withTopMap f.toZeroHom, AddHom.withTopMap f.toAddHom with toFun := WithTop.map f }
Lifting of additive monoid homomorphism to `WithTop`
Informal description
Given additive monoids \( M \) and \( N \) (both equipped with a zero element and addition operation), and an additive monoid homomorphism \( f : M \to N \), the function `AddMonoidHom.withTopMap` lifts \( f \) to an additive monoid homomorphism between the types `WithTop M` and `WithTop N`. The lifted homomorphism applies \( f \) to elements of \( M \) and preserves the top element \( \top \), while also preserving the zero element and addition operation.
WithBot.one instance
: One (WithBot α)
Full source 
@[to_additive] instance one : One (WithBot α) := WithTop.one
One Element in $\text{WithBot}\ \alpha$
Informal description
For any type $\alpha$ with a one element, the type $\text{WithBot}\ \alpha$ (which adjoins a bottom element $\bot$ to $\alpha$) also has a one element, given by the image of the one element of $\alpha$ under the canonical inclusion.
WithBot.coe_one theorem
: ((1 : α) : WithBot α) = 1
Full source 
@[to_additive (attr := simp, norm_cast)] lemma coe_one : ((1 : α) : WithBot α) = 1 := rfl
Embedding of One in WithBot Preserves Identity
Informal description
The canonical embedding of the multiplicative identity $1$ from a type $\alpha$ into $\text{WithBot}\ \alpha$ preserves the identity, i.e., $(1 : \text{WithBot}\ \alpha) = 1$.
WithBot.coe_eq_one theorem
: (a : WithBot α) = 1 ↔ a = 1
Full source 
@[to_additive (attr := simp, norm_cast)]
lemma coe_eq_one : (a : WithBot α) = 1 ↔ a = 1 := coe_eq_coe
Embedding of Element Equals One in $\text{WithBot}\,\alpha$ if and only if Element is One in $\alpha$
Informal description
For any element $a$ in $\alpha$, the canonical embedding of $a$ into $\text{WithBot}\,\alpha$ equals the multiplicative identity $1$ if and only if $a = 1$ in $\alpha$.
WithBot.one_eq_coe theorem
: 1 = (a : WithBot α) ↔ a = 1
Full source 
@[to_additive (attr := simp, norm_cast)]
lemma one_eq_coe : 1 = (a : WithBot α) ↔ a = 1 := eq_comm.trans coe_eq_one
Identity Equals Embedding in $\text{WithBot}\,\alpha$ if and only if Element is One
Informal description
For any element $a$ in $\alpha$, the multiplicative identity $1$ in $\text{WithBot}\,\alpha$ equals the canonical embedding of $a$ if and only if $a = 1$ in $\alpha$.
WithBot.bot_ne_one theorem
: (⊥ : WithBot α) ≠ 1
Full source 
@[to_additive (attr := simp)] lemma bot_ne_one : (⊥ : WithBot α) ≠ 1 := bot_ne_coe
Bottom element is distinct from one in `WithBot α`
Informal description
In the type `WithBot α` (which adjoins a bottom element $\bot$ to $\alpha$), the bottom element is not equal to the multiplicative identity element $1$.
WithBot.one_ne_bot theorem
: (1 : WithBot α) ≠ ⊥
Full source 
@[to_additive (attr := simp)] lemma one_ne_bot : (1 : WithBot α) ≠ ⊥ := coe_ne_bot
Multiplicative identity is distinct from bottom in $\text{WithBot}\ \alpha$
Informal description
In the type $\text{WithBot}\ \alpha$ (which adjoins a bottom element $\bot$ to $\alpha$), the multiplicative identity element $1$ is not equal to the bottom element $\bot$.
WithBot.unbot_one theorem
: (1 : WithBot α).unbot coe_ne_bot = 1
Full source 
@[to_additive (attr := simp)]
theorem unbot_one : (1 : WithBot α).unbot coe_ne_bot = 1 :=
  rfl
Extraction of One in $\text{WithBot}\ \alpha$ Preserves Identity
Informal description
For any type $\alpha$ with a one element, the underlying value of the multiplicative identity $1$ in $\text{WithBot}\ \alpha$ (when extracted using the `unbot` function with a proof that $1 \neq \bot$) is equal to $1$ in $\alpha$.
WithBot.unbotD_one theorem
(d : α) : (1 : WithBot α).unbotD d = 1
Full source 
@[to_additive (attr := simp)]
theorem unbotD_one (d : α) : (1 : WithBot α).unbotD d = 1 :=
  rfl
Default Extraction of One in $\text{WithBot}\ \alpha$
Informal description
For any default value $d$ of type $\alpha$, the function `unbotD` applied to the element $1$ in $\text{WithBot}\ \alpha$ returns $1$, i.e., $(1 : \text{WithBot}\ \alpha).\text{unbotD}\ d = 1$.
WithBot.one_le_coe theorem
[LE α] : 1 ≤ (a : WithBot α) ↔ 1 ≤ a
Full source 
@[to_additive (attr := simp, norm_cast) coe_nonneg]
theorem one_le_coe [LE α] : 1 ≤ (a : WithBot α) ↔ 1 ≤ a := coe_le_coe
Inequality Preservation of One in $\text{WithBot}\ \alpha$
Informal description
For any type $\alpha$ with a preorder and a one element, and for any element $a \in \alpha$, the inequality $1 \leq a$ holds in $\text{WithBot}\ \alpha$ if and only if $1 \leq a$ holds in $\alpha$.
WithBot.coe_le_one theorem
[LE α] : (a : WithBot α) ≤ 1 ↔ a ≤ 1
Full source 
@[to_additive (attr := simp, norm_cast) coe_le_zero]
theorem coe_le_one [LE α] : (a : WithBot α) ≤ 1 ↔ a ≤ 1 := coe_le_coe
Embedding Preserves Order with Respect to One in $\text{WithBot}\ \alpha$
Informal description
For any element $a$ in a type $\alpha$ equipped with a preorder, the inequality $a \leq 1$ holds in $\text{WithBot}\ \alpha$ if and only if $a \leq 1$ holds in $\alpha$.
WithBot.one_lt_coe theorem
[LT α] : 1 < (a : WithBot α) ↔ 1 < a
Full source 
@[to_additive (attr := simp, norm_cast) coe_pos]
theorem one_lt_coe [LT α] : 1 < (a : WithBot α) ↔ 1 < a := coe_lt_coe
Inequality Preservation of One in $\text{WithBot}\ \alpha$: $1 < a$
Informal description
For any element $a$ of a type $\alpha$ with a strict order, the inequality $1 < a$ holds in $\text{WithBot}\ \alpha$ if and only if $1 < a$ holds in $\alpha$.
WithBot.coe_lt_one theorem
[LT α] : (a : WithBot α) < 1 ↔ a < 1
Full source 
@[to_additive (attr := simp, norm_cast) coe_lt_zero]
theorem coe_lt_one [LT α] : (a : WithBot α) < 1 ↔ a < 1 := coe_lt_coe
Embedding Preserves Order with Respect to One in $\text{WithBot}\ \alpha$
Informal description
For any element $a$ of type $\alpha$ with a strict order, the embedding of $a$ into $\text{WithBot}\ \alpha$ is less than the multiplicative identity $1$ if and only if $a < 1$ in $\alpha$.
WithBot.map_one theorem
{β} (f : α → β) : (1 : WithBot α).map f = (f 1 : WithBot β)
Full source 
@[to_additive (attr := simp)]
protected theorem map_one {β} (f : α → β) : (1 : WithBot α).map f = (f 1 : WithBot β) :=
  rfl
Preservation of One under Lifted Map in $\text{WithBot}$
Informal description
For any function $f : \alpha \to \beta$ and the multiplicative identity element $1$ in $\text{WithBot}\ \alpha$, the image of $1$ under the lifted map $\text{WithBot.map}\ f$ equals the image of $1$ under $f$ in $\text{WithBot}\ \beta$. That is, $\text{map}\ f\ 1 = f(1)$.
WithBot.map_eq_one_iff theorem
{α} {f : α → β} {v : WithBot α} [One β] : WithBot.map f v = 1 ↔ ∃ x, v = .some x ∧ f x = 1
Full source 
@[to_additive]
theorem map_eq_one_iff {α} {f : α → β} {v : WithBot α} [One β] :
    WithBot.mapWithBot.map f v = 1 ↔ ∃ x, v = .some x ∧ f x = 1 := map_eq_some_iff
Characterization of Mapped Elements Equal to One in $\text{WithBot}$
Informal description
For any function $f : \alpha \to \beta$ and element $v \in \text{WithBot}\, \alpha$, where $\beta$ has a multiplicative identity element $1$, the following equivalence holds: $\text{map}\, f\, v = 1$ if and only if there exists $x \in \alpha$ such that $v = \text{some}\, x$ and $f(x) = 1$.
WithBot.one_eq_map_iff theorem
{α} {f : α → β} {v : WithBot α} [One β] : 1 = WithBot.map f v ↔ ∃ x, v = .some x ∧ f x = 1
Full source 
@[to_additive]
theorem one_eq_map_iff {α} {f : α → β} {v : WithBot α} [One β] :
    1 = WithBot.map f v ↔ ∃ x, v = .some x ∧ f x = 1 := some_eq_map_iff
Characterization of One Equality under Lifted Map in $\text{WithBot}$
Informal description
For any function $f : \alpha \to \beta$ and element $v \in \text{WithBot}\, \alpha$, where $\beta$ has a multiplicative identity element $1$, the following equivalence holds: $1 = \text{map}\, f\, v$ if and only if there exists $x \in \alpha$ such that $v = \text{some}\, x$ and $f(x) = 1$.
WithBot.zeroLEOneClass instance
[Zero α] [LE α] [ZeroLEOneClass α] : ZeroLEOneClass (WithBot α)
Full source 
instance zeroLEOneClass [Zero α] [LE α] [ZeroLEOneClass α] : ZeroLEOneClass (WithBot α) :=
  ⟨coe_le_coe.2 zero_le_one⟩
Preservation of Zero $\leq$ One in $\text{WithBot }\alpha$
Informal description
For any type $\alpha$ with a zero element $0$, a less-or-equal relation $\leq$, and satisfying the condition that $0 \leq 1$, the type $\text{WithBot }\alpha$ (which adjoins a bottom element $\bot$ to $\alpha$) also satisfies $0 \leq 1$.
WithBot.add instance
: Add (WithBot α)
Full source 
instance add : Add (WithBot α) :=
  ⟨Option.map₂ (· + ·)⟩
Addition Operation on Type with Bottom Element
Informal description
The type `WithBot α` can be equipped with an addition operation that extends the addition operation from `α` by defining `⊥ + x = ⊥` for any `x : WithBot α`.
WithBot.coe_add theorem
(a b : α) : ↑(a + b) = (a + b : WithBot α)
Full source 
@[simp, norm_cast] lemma coe_add (a b : α) : ↑(a + b) = (a + b : WithBot α) := rfl
Embedding Preserves Addition in `WithBot α`
Informal description
For any elements $a$ and $b$ in a type $\alpha$, the canonical embedding of their sum $a + b$ into `WithBot α` is equal to the sum of their embeddings, i.e., $\uparrow(a + b) = (\uparrow a + \uparrow b : \text{WithBot } \alpha)$.
WithBot.bot_add theorem
(x : WithBot α) : ⊥ + x = ⊥
Full source 
@[simp] lemma bot_add (x : WithBot α) : ⊥ + x = ⊥ := rfl
Bottom Element Absorbs Addition from the Left in `WithBot α`
Informal description
For any element $x$ in the type `WithBot α` (which is `α` extended with a bottom element `⊥`), the sum of the bottom element and $x$ is the bottom element, i.e., $\bot + x = \bot$.
WithBot.add_bot theorem
(x : WithBot α) : x + ⊥ = ⊥
Full source 
@[simp] lemma add_bot (x : WithBot α) : x + ⊥ = ⊥ := by cases x <;> rfl
Bottom Element Absorbs Addition from the Right in `WithBot α`
Informal description
For any element $x$ in the type `WithBot α` (which is $\alpha$ extended with a bottom element $\bot$), the sum of $x$ and the bottom element is the bottom element, i.e., $x + \bot = \bot$.
WithBot.add_eq_bot theorem
: x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
Full source 
@[simp] lemma add_eq_bot : x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥ := by cases x <;> cases y <;> simp [← coe_add]
Sum Equals Bottom if and only if Either Summand is Bottom in `WithBot α`
Informal description
For any elements $x$ and $y$ in the type `WithBot α` (which is $\alpha$ extended with a bottom element $\bot$), the sum $x + y$ equals $\bot$ if and only if either $x$ or $y$ equals $\bot$.
WithBot.add_ne_bot theorem
: x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
Full source 
lemma add_ne_bot : x + y ≠ ⊥x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥ := by cases x <;> cases y <;> simp [← coe_add]
Sum is Non-Bottom if and only if Both Summands are Non-Bottom in `WithBot α`
Informal description
For any elements $x$ and $y$ in the type `WithBot α` (which is $\alpha$ extended with a bottom element $\bot$), the sum $x + y$ is not equal to $\bot$ if and only if neither $x$ nor $y$ is equal to $\bot$.
WithBot.bot_lt_add theorem
[LT α] : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
Full source 
@[simp]
lemma bot_lt_add [LT α] : ⊥⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y := by
  simp_rw [WithBot.bot_lt_iff_ne_bot, add_ne_bot]
Bottom Element is Less Than Sum if and only if it is Less Than Both Summands
Informal description
For any elements $x$ and $y$ in `WithBot α` (where $\alpha$ is equipped with a less-than relation), the bottom element $\bot$ is less than $x + y$ if and only if $\bot$ is less than both $x$ and $y$.
WithBot.add_eq_coe theorem
: ∀ {a b : WithBot α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
Full source 
theorem add_eq_coe :
    ∀ {a b : WithBot α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
  | ⊥, b, c => by simp
  | some a, ⊥, c => by simp
  | some a, some b, c => by norm_cast; simp
Sum in `WithBot α` Equals Embedded Sum in $\alpha$
Informal description
For any elements $a, b$ in `WithBot α` (the type $\alpha$ extended with a bottom element $\bot$) and any element $c$ in $\alpha$, the sum $a + b$ equals $c$ if and only if there exist elements $a', b'$ in $\alpha$ such that $a$ is the embedding of $a'$, $b$ is the embedding of $b'$, and $a' + b' = c$ in $\alpha$.
WithBot.add_coe_eq_bot_iff theorem
: x + b = ⊥ ↔ x = ⊥
Full source 
lemma add_coe_eq_bot_iff : x + b = ⊥ ↔ x = ⊥ := by simp
Sum with Bottom Element Condition: $x + b = \bot \leftrightarrow x = \bot$
Informal description
For any element $x$ in `WithBot α` and any element $b$ in $\alpha$, the sum $x + b$ equals the bottom element $\bot$ if and only if $x$ equals $\bot$.
WithBot.coe_add_eq_bot_iff theorem
: a + y = ⊥ ↔ y = ⊥
Full source 
lemma coe_add_eq_bot_iff : a + y = ⊥ ↔ y = ⊥ := by simp
Sum with Bottom Element Condition: $a + y = \bot \leftrightarrow y = \bot$
Informal description
For any element $a$ in $\alpha$ and any element $y$ in `WithBot $\alpha$`, the sum $a + y$ equals the bottom element $\bot$ if and only if $y$ equals $\bot$.
WithBot.add_right_inj theorem
[IsRightCancelAdd α] (hz : z ≠ ⊥) : x + z = y + z ↔ x = y
Full source 
lemma add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊥) : x + z = y + z ↔ x = y := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]
Right Cancellation Law for Addition in `WithBot α` when $z \neq \bot$
Informal description
Let $\alpha$ be a type with a right cancellative addition operation, and let $x, y, z$ be elements of `WithBot α` (the type $\alpha$ extended with a bottom element $\bot$). If $z \neq \bot$, then the equation $x + z = y + z$ holds if and only if $x = y$.
WithBot.add_right_cancel theorem
[IsRightCancelAdd α] (hz : z ≠ ⊥) (h : x + z = y + z) : x = y
Full source 
lemma add_right_cancel [IsRightCancelAdd α] (hz : z ≠ ⊥) (h : x + z = y + z) : x = y :=
  (WithBot.add_right_inj hz).1 h
Right Cancellation of Addition in $\text{WithBot }\alpha$ for Non-Bottom Elements
Informal description
Let $\alpha$ be a type with a right cancellative addition operation, and let $x, y, z$ be elements of $\text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$). If $z \neq \bot$ and $x + z = y + z$, then $x = y$.
WithBot.add_left_inj theorem
[IsLeftCancelAdd α] (hx : x ≠ ⊥) : x + y = x + z ↔ y = z
Full source 
lemma add_left_inj [IsLeftCancelAdd α] (hx : x ≠ ⊥) : x + y = x + z ↔ y = z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]
Left Cancellation of Addition in $\text{WithBot }\alpha$ for Non-Bottom Elements
Informal description
Let $\alpha$ be a type with a left-cancellative addition operation, and let $x, y, z$ be elements of $\text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$). If $x \neq \bot$, then the equation $x + y = x + z$ holds if and only if $y = z$.
WithBot.add_left_cancel theorem
[IsLeftCancelAdd α] (hx : x ≠ ⊥) (h : x + y = x + z) : y = z
Full source 
lemma add_left_cancel [IsLeftCancelAdd α] (hx : x ≠ ⊥) (h : x + y = x + z) : y = z :=
  (WithBot.add_left_inj hx).1 h
Left Cancellation of Addition in $\text{WithBot }\alpha$ for Non-Bottom Elements
Informal description
Let $\alpha$ be a type with a left-cancellative addition operation, and let $x, y, z$ be elements of $\text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$). If $x \neq \bot$ and $x + y = x + z$, then $y = z$.
WithBot.addLeftMono instance
[LE α] [AddLeftMono α] : AddLeftMono (WithBot α)
Full source 
instance addLeftMono [LE α] [AddLeftMono α] : AddLeftMono (WithBot α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using (add_le_add_left · _)
Left Monotonicity of Addition in $\text{WithBot }\alpha$
Informal description
For any type $\alpha$ with a partial order $\leq$ and a left-monotonic addition operation (i.e., $b_1 \leq b_2$ implies $a + b_1 \leq a + b_2$ for all $a, b_1, b_2 \in \alpha$), the type $\text{WithBot }\alpha$ (which is $\alpha$ extended with a bottom element $\bot$) also has a left-monotonic addition operation. Specifically, for any $x, y, z \in \text{WithBot }\alpha$, if $y \leq z$, then $x + y \leq x + z$.
WithBot.addRightMono instance
[LE α] [AddRightMono α] : AddRightMono (WithBot α)
Full source 
instance addRightMono [LE α] [AddRightMono α] : AddRightMono (WithBot α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using (add_le_add_right · _)
Right Monotonicity of Addition in `WithBot α`
Informal description
For any type $\alpha$ with a partial order $\leq$ and a right-monotonic addition operation (i.e., $a_1 \leq a_2$ implies $a_1 + b \leq a_2 + b$ for all $a_1, a_2, b \in \alpha$), the type `WithBot α` (which is $\alpha$ extended with a bottom element $\bot$) also has a right-monotonic addition operation. Specifically, for any $x, y, z \in \text{WithBot }\alpha$, if $x \leq y$, then $x + z \leq y + z$.
WithBot.addLeftReflectLT instance
[LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithBot α)
Full source 
instance addLeftReflectLT [LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithBot α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_left
Addition on the Left Reflects Strict Inequalities in `WithBot α`
Informal description
For any type $\alpha$ with a strict order relation $<$ and the property that addition on the left reflects strict inequalities (i.e., $a + b_1 < a + b_2$ implies $b_1 < b_2$ for all $a, b_1, b_2 \in \alpha$), the type `WithBot α` (which is $\alpha$ extended with a bottom element $\bot$) also satisfies this property.
WithBot.addRightReflectLT instance
[LT α] [AddRightReflectLT α] : AddRightReflectLT (WithBot α)
Full source 
instance addRightReflectLT [LT α] [AddRightReflectLT α] : AddRightReflectLT (WithBot α) where
  elim x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_right
Addition on the Right Reflects Strict Inequalities in `WithBot α`
Informal description
For any type $\alpha$ with a strict order relation $<$ and the property that addition on the right reflects strict inequalities (i.e., $a_1 + b < a_2 + b$ implies $a_1 < a_2$ for all $a_1, a_2, b \in \alpha$), the type `WithBot α` (which is $\alpha$ extended with a bottom element $\bot$) also satisfies this property.
WithBot.le_of_add_le_add_left theorem
[LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : x + y ≤ x + z → y ≤ z
Full source 
protected lemma le_of_add_le_add_left [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
    x + y ≤ x + z → y ≤ z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using le_of_add_le_add_left
Left Cancellation of Addition in `WithBot α` Preserves Order
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$ and an addition operation $+$ that satisfies the left cancellation property with respect to the order (i.e., for all $a, b_1, b_2 \in \alpha$, $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$). For any elements $x, y, z \in \text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $x \neq \bot$ and $x + y \leq x + z$, then $y \leq z$.
WithBot.le_of_add_le_add_right theorem
[LE α] [AddRightReflectLE α] (hz : z ≠ ⊥) : x + z ≤ y + z → x ≤ y
Full source 
protected lemma le_of_add_le_add_right [LE α] [AddRightReflectLE α] (hz : z ≠ ⊥) :
    x + z ≤ y + z → x ≤ y := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using le_of_add_le_add_right
Right Cancellation of Addition in $\text{WithBot }\alpha$ Preserves Order
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$ and an addition operation $+$ that satisfies the right cancellation property with respect to the order (i.e., for all $a_1, a_2, b \in \alpha$, $a_1 + b \leq a_2 + b$ implies $a_1 \leq a_2$). For any elements $x, y, z \in \text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $z \neq \bot$ and $x + z \leq y + z$, then $x \leq y$.
WithBot.add_lt_add_left theorem
[LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) : y < z → x + y < x + z
Full source 
protected lemma add_lt_add_left [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) :
    y < z → x + y < x + z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using (add_lt_add_left · _)
Left Addition Preserves Strict Inequality in `WithBot α`
Informal description
Let $\alpha$ be a type with a strict order $<$ and an addition operation $+$ that is strictly monotone on the left (i.e., for all $a, b_1, b_2 \in \alpha$, $b_1 < b_2$ implies $a + b_1 < a + b_2$). For any elements $x, y, z \in \text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $x \neq \bot$ and $y < z$, then $x + y < x + z$.
WithBot.add_lt_add_right theorem
[LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) : x < y → x + z < y + z
Full source 
protected lemma add_lt_add_right [LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) :
    x < y → x + z < y + z := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using (add_lt_add_right · _)
Right Addition Preserves Strict Inequality in $\text{WithBot}\ \alpha$
Informal description
Let $\alpha$ be a type equipped with a strict order relation $<$ and an addition operation $+$ that is right strictly monotone (i.e., $a_1 < a_2$ implies $a_1 + b < a_2 + b$ for all $b \in \alpha$). For any elements $x, y, z \in \text{WithBot}\ \alpha$ where $z \neq \bot$, if $x < y$, then $x + z < y + z$.
WithBot.add_le_add_iff_left theorem
[LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : x + y ≤ x + z ↔ y ≤ z
Full source 
protected lemma add_le_add_iff_left [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
    x + y ≤ x + z ↔ y ≤ z := ⟨WithBot.le_of_add_le_add_left hx, (add_le_add_left · _)⟩
Left Cancellation of Addition in $\text{WithBot}\ \alpha$: $x + y \leq x + z \leftrightarrow y \leq z$ for $x \neq \bot$
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation $+$ that is left-monotone (i.e., $b_1 \leq b_2$ implies $a + b_1 \leq a + b_2$ for all $a, b_1, b_2 \in \alpha$) and satisfies the left cancellation property with respect to the order (i.e., $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$ for all $a, b_1, b_2 \in \alpha$). For any elements $x, y, z \in \text{WithBot}\ \alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $x \neq \bot$, then $x + y \leq x + z$ if and only if $y \leq z$.
WithBot.add_le_add_iff_right theorem
[LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊥) : x + z ≤ y + z ↔ x ≤ y
Full source 
protected lemma add_le_add_iff_right [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊥) :
    x + z ≤ y + z ↔ x ≤ y := ⟨WithBot.le_of_add_le_add_right hz, (add_le_add_right · _)⟩
Right Addition Preserves and Reflects Order in $\text{WithBot}\ \alpha$
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and an addition operation $+$ that is right-monotonic (i.e., $a_1 \leq a_2$ implies $a_1 + b \leq a_2 + b$ for all $b \in \alpha$) and reflects the order from the right (i.e., $a_1 + b \leq a_2 + b$ implies $a_1 \leq a_2$ for all $b \in \alpha$). For any elements $x, y, z \in \text{WithBot}\ \alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $z \neq \bot$, then $x + z \leq y + z$ if and only if $x \leq y$.
WithBot.add_lt_add_iff_left theorem
[LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊥) : x + y < x + z ↔ y < z
Full source 
protected lemma add_lt_add_iff_left [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊥) :
    x + y < x + z ↔ y < z := ⟨lt_of_add_lt_add_left, WithBot.add_lt_add_left hx⟩
Left Addition Preserves and Reflects Strict Inequality in $\text{WithBot }\alpha$
Informal description
Let $\alpha$ be a type with a strict order $<$ and an addition operation $+$ that is strictly monotone on the left (i.e., for all $a, b_1, b_2 \in \alpha$, $b_1 < b_2$ implies $a + b_1 < a + b_2$) and reflects strict inequalities on the left (i.e., $a + b_1 < a + b_2$ implies $b_1 < b_2$). For any elements $x, y, z \in \text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $x \neq \bot$, then $x + y < x + z$ if and only if $y < z$.
WithBot.add_lt_add_iff_right theorem
[LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ≠ ⊥) : x + z < y + z ↔ x < y
Full source 
protected lemma add_lt_add_iff_right [LT α] [AddRightStrictMono α] [AddRightReflectLT α]
    (hz : z ≠ ⊥) : x + z < y + z ↔ x < y := ⟨lt_of_add_lt_add_right, WithBot.add_lt_add_right hz⟩
Right Addition Preserves and Reflects Strict Inequality in $\text{WithBot}\ \alpha$
Informal description
Let $\alpha$ be a type with a strict order relation $<$ and an addition operation $+$ that is right strictly monotone (i.e., $a_1 < a_2$ implies $a_1 + b < a_2 + b$ for all $b \in \alpha$) and reflects strict inequalities (i.e., $a_1 + b < a_2 + b$ implies $a_1 < a_2$ for all $a_1, a_2, b \in \alpha$). For any elements $x, y, z \in \text{WithBot}\ \alpha$ where $z \neq \bot$, the inequality $x + z < y + z$ holds if and only if $x < y$.
WithBot.add_lt_add_of_le_of_lt theorem
[Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊥) (hwy : w ≤ y) (hxz : x < z) : w + x < y + z
Full source 
protected theorem add_lt_add_of_le_of_lt [Preorder α] [AddLeftStrictMono α]
    [AddRightMono α] (hw : w ≠ ⊥) (hwy : w ≤ y) (hxz : x < z) :
    w + x < y + z :=
  (WithBot.add_lt_add_left hw hxz).trans_le <| add_le_add_right hwy _
Strict Inequality Preservation in $\text{WithBot }\alpha$ under Addition with Mixed Conditions
Informal description
Let $\alpha$ be a type with a preorder $\leq$ and an addition operation $+$ that is strictly monotone on the left and monotone on the right. For any elements $w, x, y, z \in \text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $w \neq \bot$, $w \leq y$, and $x < z$, then $w + x < y + z$.
WithBot.add_lt_add_of_lt_of_le theorem
[Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊥) (hwy : w < y) (hxz : x ≤ z) : w + x < y + z
Full source 
protected theorem add_lt_add_of_lt_of_le [Preorder α] [AddLeftMono α]
    [AddRightStrictMono α] (hx : x ≠ ⊥) (hwy : w < y) (hxz : x ≤ z) :
    w + x < y + z :=
  (WithBot.add_lt_add_right hx hwy).trans_le <| add_le_add_left hxz _
Strict inequality preservation under addition in $\text{WithBot}\ \alpha$ with mixed monotonicity conditions
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$ and an addition operation $+$ such that: 1. Addition is left-monotone (i.e., $b_1 \leq b_2$ implies $a + b_1 \leq a + b_2$ for all $a, b_1, b_2 \in \alpha$) 2. Addition is right strictly monotone (i.e., $a_1 < a_2$ implies $a_1 + b < a_2 + b$ for all $b \in \alpha$) For any elements $w, x, y, z \in \text{WithBot}\ \alpha$ where $x \neq \bot$, if $w < y$ and $x \leq z$, then $w + x < y + z$.
WithBot.addLECancellable_of_ne_bot theorem
[LE α] [ContravariantClass α α (· + ·) (· ≤ ·)] (hx : x ≠ ⊥) : AddLECancellable x
Full source 
lemma addLECancellable_of_ne_bot [LE α] [ContravariantClass α α (· + ·) (· ≤ ·)]
    (hx : x ≠ ⊥) : AddLECancellable x := fun _b _c ↦ WithBot.le_of_add_le_add_left hx
Left-Order-Cancellability of Non-Bottom Elements in $\text{WithBot }\alpha$
Informal description
Let $\alpha$ be a type with a preorder $\leq$ and an addition operation $+$ such that addition is order-reflecting on the left (i.e., for all $a, b_1, b_2 \in \alpha$, $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$). For any element $x \in \text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $x \neq \bot$, then $x$ is left-order-cancellable with respect to addition, meaning that for all $y, z \in \text{WithBot }\alpha$, $x + y \leq x + z$ implies $y \leq z$.
WithBot.addLECancellable_of_lt_bot theorem
[Preorder α] [ContravariantClass α α (· + ·) (· ≤ ·)] (hx : x < ⊥) : AddLECancellable x
Full source 
lemma addLECancellable_of_lt_bot [Preorder α] [ContravariantClass α α (· + ·) (· ≤ ·)]
    (hx : x < ⊥) : AddLECancellable x := addLECancellable_of_ne_bot hx.ne
Left-Order-Cancellability of Elements Below Bottom in $\text{WithBot}\,\alpha$
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$ and an addition operation $+$ such that addition is order-reflecting on the left (i.e., for all $a, b_1, b_2 \in \alpha$, $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$). For any element $x \in \text{WithBot}\,\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), if $x < \bot$, then $x$ is left-order-cancellable with respect to addition, meaning that for all $y, z \in \text{WithBot}\,\alpha$, $x + y \leq x + z$ implies $y \leq z$.
WithBot.addLECancellable_coe theorem
[LE α] [ContravariantClass α α (· + ·) (· ≤ ·)] (a : α) : AddLECancellable (a : WithBot α)
Full source 
lemma addLECancellable_coe [LE α] [ContravariantClass α α (· + ·) (· ≤ ·)] (a : α) :
    AddLECancellable (a : WithBot α) := addLECancellable_of_ne_bot coe_ne_bot
Left-order-cancellability of embedded elements in $\text{WithBot}\,\alpha$
Informal description
Let $\alpha$ be a type with a preorder $\leq$ and an addition operation $+$ such that addition is order-reflecting on the left (i.e., for all $a, b_1, b_2 \in \alpha$, $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$). Then for any element $a \in \alpha$, its canonical embedding into $\text{WithBot}\,\alpha$ is left-order-cancellable with respect to addition, meaning that for all $y, z \in \text{WithBot}\,\alpha$, $a + y \leq a + z$ implies $y \leq z$.
WithBot.addLECancellable_iff_ne_bot theorem
[Nonempty α] [Preorder α] [ContravariantClass α α (· + ·) (· ≤ ·)] : AddLECancellable x ↔ x ≠ ⊥
Full source 
lemma addLECancellable_iff_ne_bot [Nonempty α] [Preorder α]
    [ContravariantClass α α (· + ·) (· ≤ ·)] : AddLECancellableAddLECancellable x ↔ x ≠ ⊥ where
  mp := by rintro h rfl; exact (bot_lt_coe <| Classical.arbitrary _).not_le <| h <| by simp
  mpr := addLECancellable_of_ne_bot
Characterization of Left-Order-Cancellable Elements in $\text{WithBot}\,\alpha$: $x$ is Left-Order-Cancellable if and only if $x \neq \bot$
Informal description
Let $\alpha$ be a nonempty type equipped with a preorder $\leq$ and an addition operation $+$ such that addition is order-reflecting on the left (i.e., for all $a, b_1, b_2 \in \alpha$, $a + b_1 \leq a + b_2$ implies $b_1 \leq b_2$). For any element $x$ in $\text{WithBot}\,\alpha$ (the type $\alpha$ extended with a bottom element $\bot$), $x$ is left-order-cancellable with respect to addition if and only if $x \neq \bot$. Here, an element $x$ is called *left-order-cancellable* if for all $y, z \in \text{WithBot}\,\alpha$, $x + y \leq x + z$ implies $y \leq z$.
WithBot.map_add theorem
{F} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithBot α) : (a + b).map f = a.map f + b.map f
Full source 
@[simp]
protected theorem map_add {F} [Add β] [FunLike F α β] [AddHomClass F α β]
    (f : F) (a b : WithBot α) :
    (a + b).map f = a.map f + b.map f := by
  induction a
  · exact (bot_add _).symm
  · induction b
    · exact (add_bot _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl
Preservation of Addition under Lifted Homomorphism in $\text{WithBot}\, \alpha$
Informal description
Let $\alpha$ and $\beta$ be types with addition operations, and let $F$ be a type of addition-preserving homomorphisms from $\alpha$ to $\beta$. For any $f \in F$ and any elements $a, b$ in $\text{WithBot}\, \alpha$ (the type $\alpha$ extended with a bottom element $\bot$), the map of their sum under $f$ equals the sum of their maps, i.e., $(a + b).\text{map}\, f = a.\text{map}\, f + b.\text{map}\, f$.
WithBot.AddSemigroup instance
[AddSemigroup α] : AddSemigroup (WithBot α)
Full source 
instance AddSemigroup [AddSemigroup α] : AddSemigroup (WithBot α) :=
  WithTop.addSemigroup
Additive Semigroup Structure on $\alpha \cup \{\bot\}$
Informal description
For any additive semigroup $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ forms an additive semigroup, where addition is defined by extending the addition on $\alpha$ and setting $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$.
WithBot.addCommSemigroup instance
[AddCommSemigroup α] : AddCommSemigroup (WithBot α)
Full source 
instance addCommSemigroup [AddCommSemigroup α] : AddCommSemigroup (WithBot α) :=
  WithTop.addCommSemigroup
Additive Commutative Semigroup Structure on $\alpha \cup \{\bot\}$
Informal description
For any additive commutative semigroup $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ forms an additive commutative semigroup, where addition is defined by extending the commutative addition on $\alpha$ and setting $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$.
WithBot.addZeroClass instance
[AddZeroClass α] : AddZeroClass (WithBot α)
Full source 
instance addZeroClass [AddZeroClass α] : AddZeroClass (WithBot α) :=
  WithTop.addZeroClass
Additive Zero Class Structure on $\alpha \cup \{\bot\}$
Informal description
For any type $\alpha$ equipped with an addition operation and a zero element satisfying the additive identity laws, the type $\alpha$ extended with a bottom element $\bot$ also forms an additive zero class. The addition is extended such that $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$, and the zero element is preserved.
WithBot.addMonoid instance
: AddMonoid (WithBot α)
Full source 
instance addMonoid : AddMonoid (WithBot α) := WithTop.addMonoid
Additive Monoid Structure on $\alpha \cup \{\bot\}$
Informal description
For any additive monoid $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ forms an additive monoid, where addition is defined by extending the addition on $\alpha$ and setting $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$, and the zero element is preserved.
WithBot.addHom definition
: α →+ WithBot α
Full source 
/-- Coercion from `α` to `WithBot α` as an `AddMonoidHom`. -/
def addHom : α →+ WithBot α where
  toFun := WithTop.some
  map_zero' := rfl
  map_add' _ _ := rfl
Canonical additive monoid homomorphism to $\alpha \cup \{\bot\}$
Informal description
The canonical additive monoid homomorphism from $\alpha$ to $\text{WithBot}\ \alpha$, which maps each element $a \in \alpha$ to its corresponding element in $\text{WithBot}\ \alpha$ (via the `some` constructor) and preserves the additive structure (zero and addition).
WithBot.coe_addHom theorem
: ⇑(addHom : α →+ WithBot α) = WithBot.some
Full source 
@[simp, norm_cast] lemma coe_addHom : ⇑(addHom : α →+ WithBot α) = WithBot.some := rfl
Canonical Additive Homomorphism to WithBot Equals Embedding
Informal description
The underlying function of the canonical additive monoid homomorphism from $\alpha$ to $\text{WithBot}\ \alpha$ is equal to the embedding $\text{WithBot.some} : \alpha \to \text{WithBot}\ \alpha$.
WithBot.coe_nsmul theorem
(a : α) (n : ℕ) : ↑(n • a) = n • (a : WithBot α)
Full source 
@[simp, norm_cast]
lemma coe_nsmul (a : α) (n : ℕ) : ↑(n • a) = n • (a : WithBot α) :=
  (addHom : α →+ WithBot α).map_nsmul _ _
Preservation of Scalar Multiplication under Embedding into $\alpha \cup \{\bot\}$
Informal description
For any element $a$ in an additive monoid $\alpha$ and any natural number $n$, the image of the scalar multiple $n \cdot a$ under the canonical embedding $\alpha \hookrightarrow \alpha \cup \{\bot\}$ is equal to the scalar multiple $n \cdot (a : \alpha \cup \{\bot\})$.
WithBot.addCommMonoid instance
[AddCommMonoid α] : AddCommMonoid (WithBot α)
Full source 
instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (WithBot α) :=
  WithTop.addCommMonoid
Additive Commutative Monoid Structure on $\alpha \cup \{\bot\}$
Informal description
For any additive commutative monoid $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ forms an additive commutative monoid, where addition is defined by extending the commutative addition on $\alpha$ and setting $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$.
WithBot.addMonoidWithOne instance
: AddMonoidWithOne (WithBot α)
Full source 
instance addMonoidWithOne : AddMonoidWithOne (WithBot α) := WithTop.addMonoidWithOne
Additive Monoid with One Structure on $\alpha \cup \{\bot\}$
Informal description
For any additive monoid with one $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ forms an additive monoid with one, where addition and the one element are defined by extending the operations from $\alpha$ and setting $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$, and the one element is preserved.
WithBot.coe_natCast theorem
(n : ℕ) : ((n : α) : WithBot α) = n
Full source 
@[norm_cast] lemma coe_natCast (n : ℕ) : ((n : α) : WithBot α) = n := rfl
Embedding of Natural Numbers Preserves Identity in $\alpha \cup \{\bot\}$
Informal description
For any natural number $n$, the canonical embedding of $n$ into $\alpha \cup \{\bot\}$ (where $\alpha$ is an additive monoid with one) is equal to $n$ itself, i.e., $(n : \alpha) = n$ in $\alpha \cup \{\bot\}$.
WithBot.natCast_ne_bot theorem
(n : ℕ) : (n : WithBot α) ≠ ⊥
Full source 
@[simp] lemma natCast_ne_bot (n : ℕ) : (n : WithBot α) ≠ ⊥ := coe_ne_bot
Natural number embeddings are distinct from bottom in $\alpha \cup \{\bot\}$
Informal description
For any natural number $n$, the canonical embedding of $n$ into $\alpha \cup \{\bot\}$ is not equal to the bottom element $\bot$.
WithBot.bot_ne_natCast theorem
(n : ℕ) : (⊥ : WithBot α) ≠ n
Full source 
@[simp] lemma bot_ne_natCast (n : ℕ) : (⊥ : WithBot α) ≠ n := bot_ne_coe
Bottom element is distinct from any natural number in $\alpha \cup \{\bot\}$
Informal description
For any natural number $n$, the bottom element $\bot$ in $\alpha \cup \{\bot\}$ is not equal to the embedding of $n$ into $\alpha \cup \{\bot\}$.
WithBot.coe_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : α) : WithBot α) = ofNat(n)
Full source 
@[simp] lemma coe_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : α) : WithBot α) = ofNat(n) := rfl
Commutativity of numeral embedding through WithBot construction
Informal description
For any natural number $n \geq 2$ and any type $\alpha$ with a canonical interpretation of numerals, the embedding of the numeral $n$ into $\alpha$ followed by the embedding into $\alpha \cup \{\bot\}$ (via `WithBot.some`) equals the direct interpretation of $n$ in $\alpha \cup \{\bot\}$. In other words, the following diagram commutes: $$\text{ofNat}(n) \in \alpha \xrightarrow{\text{WithBot.some}} \text{WithBot}(\alpha) = \text{ofNat}(n) \in \text{WithBot}(\alpha)$$
WithBot.coe_eq_ofNat theorem
(n : ℕ) [n.AtLeastTwo] (m : α) : (m : WithBot α) = ofNat(n) ↔ m = ofNat(n)
Full source 
@[simp] lemma coe_eq_ofNat (n : ℕ) [n.AtLeastTwo] (m : α) :
    (m : WithBot α) = ofNat(n) ↔ m = ofNat(n) :=
  coe_eq_coe
Embedding Equality Criterion in $\alpha \cup \{\bot\}$ for Numerals $\geq 2$
Informal description
For any natural number $n \geq 2$ and any element $m$ of type $\alpha$, the canonical embedding of $m$ into $\text{WithBot}\,\alpha$ equals the canonical embedding of $n$ if and only if $m$ equals $n$ in $\alpha$.
WithBot.ofNat_eq_coe theorem
(n : ℕ) [n.AtLeastTwo] (m : α) : ofNat(n) = (m : WithBot α) ↔ ofNat(n) = m
Full source 
@[simp] lemma ofNat_eq_coe (n : ℕ) [n.AtLeastTwo] (m : α) :
    ofNat(n)ofNat(n) = (m : WithBot α) ↔ ofNat(n) = m :=
  coe_eq_coe
Equality of Numerals and Embeddings in $\alpha \cup \{\bot\}$
Informal description
For any natural number $n \geq 2$ and any element $m$ of type $\alpha$, the numeral $n$ in $\text{WithBot}\,\alpha$ equals the embedding of $m$ if and only if $n$ equals $m$ in $\alpha$.
WithBot.ofNat_ne_bot theorem
(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : WithBot α) ≠ ⊥
Full source 
@[simp] lemma ofNat_ne_bot (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : WithBot α) ≠ ⊥ :=
  natCast_ne_bot n
Embedded Numerals are Distinct from Bottom in $\alpha \cup \{\bot\}$
Informal description
For any natural number $n \geq 2$, the canonical embedding of $n$ into $\alpha \cup \{\bot\}$ is not equal to the bottom element $\bot$.
WithBot.bot_ne_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : (⊥ : WithBot α) ≠ ofNat(n)
Full source 
@[simp] lemma bot_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊥ : WithBot α) ≠ ofNat(n) :=
  bot_ne_natCast n
Bottom element distinct from numerals ≥ 2 in $\alpha \cup \{\bot\}$
Informal description
For any natural number $n \geq 2$ and any type $\alpha$, the bottom element $\bot$ in $\alpha \cup \{\bot\}$ is not equal to the embedded numeral $n$.
WithBot.map_ofNat theorem
{f : α → β} (n : ℕ) [n.AtLeastTwo] : WithBot.map f (ofNat(n) : WithBot α) = f ofNat(n)
Full source 
@[simp] lemma map_ofNat {f : α → β} (n : ℕ) [n.AtLeastTwo] :
    WithBot.map f (ofNat(n) : WithBot α) = f ofNat(n) := map_coe f n
Lifted Function Evaluation on Numerals in $\text{WithBot}\, \alpha$
Informal description
For any function $f : \alpha \to \beta$ and any natural number $n \geq 2$, the lifted function $\text{map}\, f$ applied to the embedded numeral $n$ in $\text{WithBot}\, \alpha$ equals $f$ applied to $n$, i.e., $\text{map}\, f\, n = f(n)$.
WithBot.map_natCast theorem
{f : α → β} (n : ℕ) : WithBot.map f (n : WithBot α) = f n
Full source 
@[simp] lemma map_natCast {f : α → β} (n : ℕ) :
    WithBot.map f (n : WithBot α) = f n := map_coe f n
Lifted Function Evaluation on Natural Numbers in `WithBot`
Informal description
For any function $f \colon \alpha \to \beta$ and any natural number $n \in \mathbb{N}$, the lifted function $\text{map}\, f$ on $\text{WithBot}\, \alpha$ maps the natural number $n$ (embedded in $\text{WithBot}\, \alpha$) to $f(n)$, i.e., $\text{map}\, f\, n = f(n)$.
WithBot.map_eq_ofNat_iff theorem
{f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} : a.map f = ofNat(n) ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma map_eq_ofNat_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
    a.map f = ofNat(n) ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
Characterization of when a lifted function equals a numeral in $\alpha \cup \{\bot\}$
Informal description
Let $f : \beta \to \alpha$ be a function, $n \geq 2$ a natural number, and $a \in \beta \cup \{\bot\}$. Then the following are equivalent: 1. The lifted function $\text{map}\, f$ applied to $a$ equals the canonical embedding of $n$ in $\alpha \cup \{\bot\}$. 2. There exists $x \in \beta$ such that $a = x$ (i.e., $a$ is not $\bot$) and $f(x) = n$. In symbols: $$ \text{map}\, f\, a = n \leftrightarrow \exists x \in \beta,\ a = x \land f(x) = n $$
WithBot.ofNat_eq_map_iff theorem
{f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} : ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma ofNat_eq_map_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
    ofNat(n)ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
Characterization of Numeral Equality under Lifted Mapping in $\alpha \cup \{\bot\}$
Informal description
For any function $f : \beta \to \alpha$, natural number $n \geq 2$, and element $a \in \text{WithBot}\, \beta$, the following equivalence holds: The numeral $n$ (interpreted in $\text{WithBot}\, \alpha$) equals the image of $a$ under the lifted map $\text{map}\, f$ if and only if there exists $x \in \beta$ such that $a = \text{some}\, x$ and $f(x) = n$.
WithBot.map_eq_natCast_iff theorem
{f : β → α} {n : ℕ} {a : WithBot β} : a.map f = n ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma map_eq_natCast_iff {f : β → α} {n : ℕ} {a : WithBot β} :
    a.map f = n ↔ ∃ x, a = .some x ∧ f x = n := map_eq_some_iff
Characterization of Natural Number Cast in `WithBot` via Mapping
Informal description
For any function $f : \beta \to \alpha$, natural number $n \in \mathbb{N}$, and element $a \in \text{WithBot}\, \beta$, the following equivalence holds: $\text{map}\, f\, a = n$ if and only if there exists $x \in \beta$ such that $a = \text{some}\, x$ and $f(x) = n$.
WithBot.natCast_eq_map_iff theorem
{f : β → α} {n : ℕ} {a : WithBot β} : n = a.map f ↔ ∃ x, a = .some x ∧ f x = n
Full source 
lemma natCast_eq_map_iff {f : β → α} {n : ℕ} {a : WithBot β} :
    n = a.map f ↔ ∃ x, a = .some x ∧ f x = n := some_eq_map_iff
Characterization of Natural Number Cast in `WithBot` via Mapping
Informal description
For any function $f \colon \beta \to \alpha$, natural number $n \in \mathbb{N}$, and element $a \in \beta \cup \{\bot\}$, the following equivalence holds: \[ n = \text{map}\, f\, a \quad \text{if and only if} \quad \exists x \in \beta, \ a = x \ \text{and} \ f(x) = n. \] Here, $\text{map}\, f\, a$ applies $f$ to the value in $\beta$ if $a \neq \bot$, and returns $\bot$ otherwise.
WithBot.charZero instance
[AddMonoidWithOne α] [CharZero α] : CharZero (WithBot α)
Full source 
instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithBot α) :=
  WithTop.charZero
Characteristic Zero Preservation in $\alpha \cup \{\bot\}$
Informal description
For any additive monoid with one $\alpha$ of characteristic zero, the type $\alpha$ extended with a bottom element $\bot$ also has characteristic zero. This means the canonical map from natural numbers to $\text{WithBot}\ \alpha$ is injective.
WithBot.addCommMonoidWithOne instance
[AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithBot α)
Full source 
instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithBot α) :=
  WithTop.addCommMonoidWithOne
Additive Commutative Monoid with One Structure on $\alpha \cup \{\bot\}$
Informal description
For any additive commutative monoid with one $\alpha$, the type $\alpha$ extended with a bottom element $\bot$ forms an additive commutative monoid with one, where addition and the one element are defined by extending the operations from $\alpha$ and setting $\bot + a = a + \bot = \bot$ for any $a \in \alpha \cup \{\bot\}$.
OneHom.withBotMap definition
{M N : Type*} [One M] [One N] (f : OneHom M N) : OneHom (WithBot M) (WithBot N)
Full source 
/-- A version of `WithBot.map` for `OneHom`s. -/
@[to_additive (attr := simps -fullyApplied)
  "A version of `WithBot.map` for `ZeroHom`s"]
protected def _root_.OneHom.withBotMap {M N : Type*} [One M] [One N] (f : OneHom M N) :
    OneHom (WithBot M) (WithBot N) where
  toFun := WithBot.map f
  map_one' := by rw [WithBot.map_one, map_one, coe_one]
Lifting of identity-preserving homomorphism to `WithBot`
Informal description
Given an identity-preserving homomorphism $f \colon M \to N$ between types with distinguished elements $1$, this defines the lifted homomorphism $\text{WithBot} M \to \text{WithBot} N$ that extends $f$ by mapping the bottom element $\bot$ to itself and preserves the identity element (i.e., maps $1$ to $1$).
AddHom.withBotMap definition
{M N : Type*} [Add M] [Add N] (f : AddHom M N) : AddHom (WithBot M) (WithBot N)
Full source 
/-- A version of `WithBot.map` for `AddHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddHom.withBotMap {M N : Type*} [Add M] [Add N] (f : AddHom M N) :
    AddHom (WithBot M) (WithBot N) where
  toFun := WithBot.map f
  map_add' := WithBot.map_add f
Lifting of additive homomorphism to `WithBot`
Informal description
Given an additive homomorphism $f \colon M \to N$ between types equipped with addition operations, this defines the lifted additive homomorphism $\text{WithBot} M \to \text{WithBot} N$ that extends $f$ by mapping the bottom element $\bot$ to itself and preserves addition on non-bottom elements.
AddMonoidHom.withBotMap definition
{M N : Type*} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : WithBot M →+ WithBot N
Full source 
/-- A version of `WithBot.map` for `AddMonoidHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddMonoidHom.withBotMap {M N : Type*} [AddZeroClass M] [AddZeroClass N]
    (f : M →+ N) : WithBotWithBot M →+ WithBot N :=
  { ZeroHom.withBotMap f.toZeroHom, AddHom.withBotMap f.toAddHom with toFun := WithBot.map f }
Lifting of additive monoid homomorphism to `WithBot`
Informal description
Given an additive monoid homomorphism $f \colon M \to N$ between additive monoids, this defines the lifted additive monoid homomorphism $\text{WithBot} M \to \text{WithBot} N$ that extends $f$ by mapping the bottom element $\bot$ to itself and preserves both the zero element and addition on non-bottom elements.