some_eq_coe — Mathlib

English

The natural embedding of natural numbers into ENNat coincides with the canonical casting of naturals into ENNat.

Русский

Встраивание натуральных чисел в ENat совпадает с каноническим приведениям натуральных чисел к ENat.

LaTeX

$$$$\\operatorname{NatCast}_{\\mathbb{N} \\to \\mathbb{N}_{\\infty}}(n) = \\operatorname{WithTop}.\\mathrm{some}(n) \\quad\\text{for all } n \\in \\mathbb{N}.$$$$

Lean4

/-- Lemmas about `WithTop` expect (and can output) `WithTop.some` but the normal form for coercion
`ℕ → ℕ∞` is `Nat.cast`. -/
@[simp]
theorem some_eq_coe : (WithTop.some : ℕ → ℕ∞) = Nat.cast :=
  rfl

Похожие утверждения