cast_eq_cast — Mathlib

English

For h : n = m, the map Fin.cast h equals the standard cast map built from h.

Русский

Для h : n = m отображение Fin.cast h совпадает с обычным отображением приведения, построенным через h.

LaTeX

$$$$ \\forall {n m : \\mathbb{N}} (h : n = m), \\ (\\mathrm{Fin.cast}\\,h) = \\_\\root\\cast (h \\,\\triangleright\\, \\mathrm{rfl}). $$$$

Lean4

/-- While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply
a generic theorem about `cast`. -/
theorem cast_eq_cast (h : n = m) : (Fin.cast h : Fin n → Fin m) = _root_.cast (h ▸ rfl) :=
  by
  subst h
  ext
  rfl

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