Definition and basic properties of extended natural numbers #
In this file we define enat
(notation: ℕ∞
) to be with_top ℕ
and prove some basic lemmas
about this type.
Extended natural numbers ℕ∞ = with_top ℕ
.
Instances for enat
- enat.has_zero
- enat.add_comm_monoid_with_one
- enat.canonically_ordered_comm_semiring
- enat.nontrivial
- enat.linear_order
- enat.order_bot
- enat.order_top
- enat.has_bot
- enat.has_top
- enat.canonically_linear_ordered_add_monoid
- enat.has_sub
- enat.has_ordered_sub
- enat.complete_linear_order
- enat.linear_ordered_add_comm_monoid_with_top
- enat.succ_order
- enat.inhabited
- enat.nat.can_lift
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- enat.inhabited = {default := 0}
@[protected, instance]
Equations
Conversion of ℕ∞
to ℕ
sending ∞
to 0
.
Equations
- enat.to_nat = {to_fun := with_top.untop' 0, map_zero' := enat.to_nat._proof_1, map_one' := enat.to_nat._proof_2, map_mul' := enat.to_nat._proof_3}