English
There is a computable embedding of the natural numbers into PartENat, given by some(n) = Part.some(n), aligning with the natural coercion.
Русский
Существует вычислимое вложение ℕ в PartENat, заданное some(n) = Part.some(n), согласующееся с естественным включением ℕ в PartENat.
LaTeX
$$$ \operatorname{some} : \mathbb{N} \to \operatorname{PartENat}, \quad \operatorname{some}(n) = \operatorname{Part.some}(n). $$$
Lean4
/-- The computable embedding `ℕ → PartENat`.
This coincides with the coercion `coe : ℕ → PartENat`, see `PartENat.some_eq_natCast`. -/
@[coe]
def some : ℕ → PartENat :=
Part.some
