mathlib documentation

data.nat.with_bot

`with_bot ℕ`

Lemmas about the type of natural numbers with a bottom element adjoined.

theorem nat.with_bot.add_eq_zero_iff {n m : with_bot ℕ} :

n + m = 0 ↔ n = 0 ∧ m = 0

theorem nat.with_bot.add_eq_one_iff {n m : with_bot ℕ} :

n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

@[simp]

theorem nat.with_bot.coe_nonneg {n : ℕ} :

@[simp]

theorem nat.with_bot.lt_zero_iff (n : with_bot ℕ) :

n < 0 ↔ n = ⊥