Definition and basic properties of extended natural numbers #
In this file we define ENat
(notation: ℕ∞
) to be WithTop ℕ
and prove some basic lemmas
about this type.
Implementation details #
There are two natural coercions from ℕ
to WithTop ℕ = ENat
: WithTop.some
and Nat.cast
. In
Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally
equal, we did not duplicate generic lemmas about WithTop α
and WithTop.some
coercion for ENat
and Nat.cast
coercion. If you need to apply a lemma about WithTop
, you may either rewrite back
and forth using ENat.some_eq_coe
, or restate the lemma for ENat
.
@[simp]
Lemmas about WithTop
expect (and can output) WithTop.some
but the normal form for coercion
ℕ → ℕ∞
is Nat.cast
.
@[simp]
theorem
ENat.recTopCoe_top
{C : ℕ∞ → Sort u_1}
(d : C ⊤)
(f : (a : ℕ) → C ↑a)
:
ENat.recTopCoe d f ⊤ = d
@[simp]
theorem
ENat.recTopCoe_coe
{C : ℕ∞ → Sort u_1}
(d : C ⊤)
(f : (a : ℕ) → C ↑a)
(x : ℕ)
:
ENat.recTopCoe d f ↑x = f x
Alias of the reverse direction of ENat.coe_toNat_eq_self
.
theorem
ENat.toNat_add
{m : ℕ∞}
{n : ℕ∞}
(hm : m ≠ ⊤)
(hn : n ≠ ⊤)
:
↑ENat.toNat (m + n) = ↑ENat.toNat m + ↑ENat.toNat n
theorem
ENat.toNat_sub
{n : ℕ∞}
(hn : n ≠ ⊤)
(m : ℕ∞)
:
↑ENat.toNat (m - n) = ↑ENat.toNat m - ↑ENat.toNat n