coe_eq_castSucc — Mathlib

English

For any a in Fin(n), the natural embedding of a into Fin(n+1) coincides with castSucc(a).

Русский

Для любого a ∈ Fin(n) каноническое вложение a в Fin(n+1) совпадает с castSucc(a).

LaTeX

$$$$ \\forall n \\in \\mathbb{N}, \\forall a \\in \\mathrm{Fin}(n): ((a : \\mathbb{N}) : \\mathrm{Fin}(n+1)) = \\operatorname{castSucc}(a). $$$$

Lean4

@[norm_cast, simp]
theorem coe_eq_castSucc {a : Fin n} : ((a : Nat) : Fin (n + 1)) = castSucc a :=
  by
  ext
  exact val_cast_of_lt (Nat.lt.step a.is_lt)

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