Successor bounds in extended natural numbers

Krull dimensions take values in WithBot ℕ∞, and a dimension formula often has the shape c + 1 = k for a natural number k. In WithBot ℕ∞ the inequality c < c + 1 fails for c = ⊤, but a successor equal to a natural number rules that case out, so c < k.

A successor bound in ℕ∞ also gives a nonzero order after coercion to WithTop ℕ∞.

Main results

• ENat.coe_ne_zero_of_add_one_le: a successor bound gives a nonzero extended order.
• ENat.WithBot.lt_natCast_of_add_one_eq: if c + 1 = k with k : ℕ, then c < k.

theorem ENat.coe_ne_zero_of_add_one_le {n r : ℕ∞} (h : n + 1 ≤ r) : ↑r ≠ 0

An extended order above a successor remains nonzero after adjoining a new top element.

theorem ENat.WithBot.lt_natCast_of_add_one_eq {c : WithBot ℕ∞} {k : ℕ} (h : c + 1 = ↑k) : c < ↑k

In WithBot ℕ∞, an element whose successor is a natural number is smaller than it.