Natural numbers with infinity #
The natural numbers and an extra top
element ⊤
. This implementation uses Part ℕ
as an
implementation. Use ℕ∞
instead unless you care about computability.
Main definitions #
The following instances are defined:
There is no additive analogue of MonoidWithZero
; if there were then PartENat
could
be an AddMonoidWithTop
.
-
toWithTop
: the map fromPartENat
toℕ∞
, with theorems that it plays well with+
and≤
. -
withTopAddEquiv : PartENat ≃+ ℕ∞
-
withTopOrderIso : PartENat ≃o ℕ∞
Implementation details #
PartENat
is defined to be Part ℕ
.
+
and ≤
are defined on PartENat
, but there is an issue with *
because it's not
clear what 0 * ⊤
should be. mul
is hence left undefined. Similarly ⊤ - ⊤
is ambiguous
so there is no -
defined on PartENat
.
Before the open Classical
line, various proofs are made with decidability assumptions.
This can cause issues -- see for example the non-simp lemma toWithTopZero
proved by rfl
,
followed by @[simp] lemma toWithTopZero'
whose proof uses convert
.
Tags #
PartENat, ℕ∞
The computable embedding ℕ → PartENat
.
This coincides with the coercion coe : ℕ → PartENat
, see PartENat.some_eq_natCast
.
Instances For
Equiv
between PartENat
and ℕ∞
(for the order isomorphism see
withTopOrderIso
).
Instances For
The smallest PartENat
satisfying a (decidable) predicate P : ℕ → Prop