ofNat_fst — Mathlib

English

For n with AtLeastTwo, the first coordinate of ofNat(n) equals the canonical nat-cast, i.e., fst(ofNat(n)) = OfNat.ofNat n.

Русский

Для n, удовлетворяющего AtLeastTwo, первая координата ofNat(n) равна каноническому натуральному отображению, fst(ofNat(n)) = OfNat.ofNat n.

LaTeX

$$$\text{fst}(\operatorname{ofNat}(n)) = \operatorname{OfNat}(n)$$$

Lean4

@[simp]
theorem ofNat_fst (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : X q).fst = OfNat.ofNat n :=
  rfl

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