Documentation

Mathlib.Data.ENat.SuccOrder

SuccOrder structure on ENat #

source
@[instance_reducible]
instance instSuccOrderENat :
SuccOrder ℕ∞
Equations
source
@[simp]
theorem ENat.succ_natCast (n : ℕ) :
SuccOrder.succ ↑n = ↑(n + 1)
source
@[deprecated ENat.succ_natCast (since := "2026-07-17")]
theorem ENat.succ_coe (n : ℕ) :
SuccOrder.succ ↑n = ↑(n + 1)

Alias of ENat.succ_natCast.

source
@[simp]
theorem ENat.succ_top :
SuccOrder.succ ⊤ = ⊤
source
@[instance_reducible]
instance ENat.instSuccAddOrder :
SuccAddOrder ℕ∞
Equations
source
@[deprecated Order.succ_eq_add_one (since := "2026-05-25")]
theorem ENat.succ_def (m : ℕ∞) :
Order.succ m = m + 1
source
theorem ENat.add_one_le_iff {m n : ℕ∞} (hm : m ≠ ⊤) :
m + 1 ≤ n ↔ m < n
source
theorem ENat.add_one_le_iff' {m n : ℕ∞} (hn : n ≠ ⊤) :
m + 1 ≤ n ↔ m < n
source
theorem ENat.natCast_add_one_le_iff {m : ℕ} {n : ℕ∞} :
↑m + 1 ≤ n ↔ ↑m < n
source
@[deprecated ENat.natCast_add_one_le_iff (since := "2026-07-17")]
theorem ENat.coe_add_one_le_iff {m : ℕ} {n : ℕ∞} :
↑m + 1 ≤ n ↔ ↑m < n

Alias of ENat.natCast_add_one_le_iff.

source
theorem ENat.add_one_le_natCast_iff {m : ℕ∞} {n : ℕ} :
m + 1 ≤ ↑n ↔ m < ↑n
source
@[deprecated ENat.add_one_le_natCast_iff (since := "2026-07-17")]
theorem ENat.add_one_le_coe_iff {m : ℕ∞} {n : ℕ} :
m + 1 ≤ ↑n ↔ m < ↑n

Alias of ENat.add_one_le_natCast_iff.

source
@[deprecated Order.one_le_iff_ne_zero (since := "2026-05-25")]
theorem ENat.one_le_iff_ne_zero {n : ℕ∞} :
1 ≤ n ↔ n ≠ 0
source
@[deprecated Order.lt_one_iff (since := "2026-05-25")]
theorem ENat.lt_one_iff_eq_zero {n : ℕ∞} :
n < 1 ↔ n = 0
source
@[deprecated Order.le_one_iff (since := "2026-05-25")]
theorem ENat.le_one_iff_eq_zero_or_eq_one {n : ℕ∞} :
n ≤ 1 ↔ n = 0 ∨ n = 1
source
theorem ENat.lt_add_one_iff {m n : ℕ∞} (hn : n ≠ ⊤) :
m < n + 1 ↔ m ≤ n
source
theorem ENat.lt_add_one_iff' {m n : ℕ∞} (hm : m ≠ ⊤) :
m < n + 1 ↔ m ≤ n
source
@[simp]
theorem ENat.lt_two_iff {n : ℕ∞} :
n < 2 ↔ n ≤ 1
source
theorem ENat.lt_natCast_add_one_iff {m : ℕ∞} {n : ℕ} :
m < ↑n + 1 ↔ m ≤ ↑n
source
@[deprecated ENat.lt_natCast_add_one_iff (since := "2026-07-17")]
theorem ENat.lt_coe_add_one_iff {m : ℕ∞} {n : ℕ} :
m < ↑n + 1 ↔ m ≤ ↑n

Alias of ENat.lt_natCast_add_one_iff.

source
theorem ENat.natCast_lt_add_one_iff {m : ℕ} {n : ℕ∞} :
↑m < n + 1 ↔ ↑m ≤ n
source
@[deprecated ENat.natCast_lt_add_one_iff (since := "2026-07-17")]
theorem ENat.coe_lt_add_one_iff {m : ℕ} {n : ℕ∞} :
↑m < n + 1 ↔ ↑m ≤ n

Alias of ENat.natCast_lt_add_one_iff.

source
theorem ENat.le_sub_one_of_lt {a b : ℕ∞} (h : a < b) :
a ≤ b - 1
source
theorem ENat.WithBot.lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} :
n < ↑m + 1 ↔ n ≤ ↑m
source
theorem ENat.WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} :
↑n + 1 ≤ m ↔ ↑n < m
source
theorem ENat.WithBot.add_one_le_natCast_iff {n : WithBot ℕ∞} {m : ℕ} :
n + 1 ≤ ↑m ↔ n < ↑m
source
@[simp]
theorem ENat.WithBot.add_one_le_zero_iff (n : WithBot ℕ∞) :
n + 1 ≤ 0 ↔ n = ⊥