scilib documentation

data.nat.with_bot

with_bot ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
theorem nat.with_bot.add_eq_zero_iff {n m : with_bot ℕ} :
n + m = 0 ↔ n = 0 ∧ m = 0
source
theorem nat.with_bot.add_eq_one_iff {n m : with_bot ℕ} :
n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
source
theorem nat.with_bot.add_eq_two_iff {n m : with_bot ℕ} :
n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
source
theorem nat.with_bot.add_eq_three_iff {n m : with_bot ℕ} :
n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
source
theorem nat.with_bot.coe_nonneg {n : ℕ} :
0 ≤ ↑n
source
@[simp]
theorem nat.with_bot.lt_zero_iff (n : with_bot ℕ) :
n < 0 ↔ n = ⊥
source
theorem nat.with_bot.one_le_iff_zero_lt {x : with_bot ℕ} :
1 ≤ x ↔ 0 < x
source
theorem nat.with_bot.lt_one_iff_le_zero {x : with_bot ℕ} :
x < 1 ↔ x ≤ 0
source
theorem nat.with_bot.add_one_le_of_lt {n m : with_bot ℕ} (h : n < m) :
n + 1 ≤ m