some_eq_natCast — Mathlib

English

The natural embedding of ℕ into PartENat coincides with the canonical nat cast; for every n, some n equals n in PartENat.

Русский

Естественное вложение ℕ в PartENat совпадает с каноническим отображением; для каждого n элемент some n равен n в PartENat.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, (\\\\mathrm{some}\\\\, n) = n$$$

Lean4

theorem some_eq_natCast (n : ℕ) : some n = n :=
  rfl

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