Definition and basic properties of extended natural numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define
ℕ∞) to be
with_top ℕ and prove some basic lemmas
about this type.
Extended natural numbers
ℕ∞ = with_top ℕ.