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 = ⊥

theorem nat.with_bot.one_le_iff_zero_lt {x : with_bot ℕ} :

1 ≤ x ↔ 0 < x

theorem nat.with_bot.lt_one_iff_le_zero {x : with_bot ℕ} :

x < 1 ↔ x ≤ 0