Mathlib.Data.Nat.WithBot

Nat.WithBot.instWellFoundedRelationWithBot instance

: WellFoundedRelation (WithBot ℕ)

Full source

instance : WellFoundedRelation (WithBot ℕ) where
  rel := (· < ·)
  wf := IsWellFounded.wf

Well-Founded Relation on $\mathbb{N} \cup \{\bot\}$

Informal description

The type $\mathbb{N} \cup \{\bot\}$ (natural numbers with a bottom element adjoined) has a well-founded relation.

Nat.WithBot.add_eq_zero_iff theorem

{n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0

Full source

theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := by
  cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, add_eq_zero_iff_of_nonneg]

Sum in $\mathbb{N} \cup \{\bot\}$ equals zero if and only if both summands are zero

Informal description

For any two elements $n$ and $m$ in $\mathbb{N} \cup \{\bot\}$, the sum $n + m$ equals $0$ if and only if both $n = 0$ and $m = 0$.

Nat.WithBot.add_eq_one_iff theorem

{n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

Full source

theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by
  cases n
  · simp only [WithBot.bot_add, WithBot.bot_ne_one, WithBot.bot_ne_zero, false_and, or_self]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_one_iff]

Sum Equals One in Extended Natural Numbers

Informal description

For any two elements $n$ and $m$ in $\mathbb{N} \cup \{\bot\}$, the sum $n + m$ equals $1$ if and only if either $n = 0$ and $m = 1$, or $n = 1$ and $m = 0$.

Nat.WithBot.add_eq_two_iff theorem

{n m : WithBot ℕ} : n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0

Full source

theorem add_eq_two_iff {n m : WithBot ℕ} :
    n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 := by
  cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_two_iff]

Sum Equals Two in Extended Natural Numbers

Informal description

For any two elements $n$ and $m$ in $\mathbb{N} \cup \{\bot\}$, the sum $n + m$ equals $2$ if and only if one of the following holds: - $n = 0$ and $m = 2$, - $n = 1$ and $m = 1$, - $n = 2$ and $m = 0$.

Nat.WithBot.add_eq_three_iff theorem

{n m : WithBot ℕ} : n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0

Full source

theorem add_eq_three_iff {n m : WithBot ℕ} :
    n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0 := by
  cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_three_iff]

Sum Equals Three in Extended Natural Numbers

Informal description

For any two elements $n$ and $m$ in $\mathbb{N} \cup \{\bot\}$, the sum $n + m$ equals $3$ if and only if one of the following holds: - $n = 0$ and $m = 3$, - $n = 1$ and $m = 2$, - $n = 2$ and $m = 1$, - $n = 3$ and $m = 0$.

Nat.WithBot.coe_nonneg theorem

{n : ℕ} : 0 ≤ (n : WithBot ℕ)

Full source

theorem coe_nonneg {n : ℕ} : 0 ≤ (n : WithBot ℕ) := by
  rw [← WithBot.coe_zero, cast_withBot, WithBot.coe_le_coe]
  exact n.zero_le

Nonnegativity of Canonical Embedding in Extended Natural Numbers

Informal description

For any natural number $n$, the canonical embedding of $n$ into the extended natural numbers with a bottom element satisfies $0 \leq n$.

Nat.WithBot.lt_zero_iff theorem

{n : WithBot ℕ} : n < 0 ↔ n = ⊥

Full source

@[simp]
theorem lt_zero_iff {n : WithBot ℕ} : n < 0 ↔ n = ⊥ := WithBot.lt_coe_bot

Characterization of Elements Less Than Zero in Extended Natural Numbers

Informal description

For any element $n$ in $\mathbb{N} \cup \{\bot\}$, the inequality $n < 0$ holds if and only if $n$ is the bottom element $\bot$.

Nat.WithBot.one_le_iff_zero_lt theorem

{x : WithBot ℕ} : 1 ≤ x ↔ 0 < x

Full source

theorem one_le_iff_zero_lt {x : WithBot ℕ} : 1 ≤ x ↔ 0 < x := by
  refine ⟨zero_lt_one.trans_le, fun h => ?_⟩
  cases x
  · exact (not_lt_bot h).elim
  · rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h

Characterization of One Less Than or Equal to $x$ in Extended Natural Numbers via Zero Less Than $x$

Informal description

For any element $x$ in the extended natural numbers $\mathbb{N} \cup \{\bot\}$, the inequality $1 \leq x$ holds if and only if $0 < x$.

Nat.WithBot.lt_one_iff_le_zero theorem

{x : WithBot ℕ} : x < 1 ↔ x ≤ 0

Full source

theorem lt_one_iff_le_zero {x : WithBot ℕ} : x < 1 ↔ x ≤ 0 :=
  not_iff_not.mp (by simpa using one_le_iff_zero_lt)

Characterization of Elements Less Than One in Extended Natural Numbers via Non-Positivity

Informal description

For any element $x$ in the extended natural numbers $\mathbb{N} \cup \{\bot\}$, the inequality $x < 1$ holds if and only if $x \leq 0$.

Nat.WithBot.add_one_le_of_lt theorem

{n m : WithBot ℕ} (h : n < m) : n + 1 ≤ m

Full source

theorem add_one_le_of_lt {n m : WithBot ℕ} (h : n < m) : n + 1 ≤ m := by
  cases n
  · simp only [WithBot.bot_add, bot_le]
  cases m
  · exact (not_lt_bot h).elim
  · rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
      WithBot.coe_one] at h

Successor Inequality in Extended Natural Numbers: $n < m \Rightarrow n + 1 \leq m$

Informal description

For any two extended natural numbers $n$ and $m$ (i.e., elements of $\mathbb{N} \cup \{\bot\}$), if $n < m$, then $n + 1 \leq m$.