cast_eq_cast' — Mathlib

English

If Fin n = Fin m, then cast h equals Fin.cast (fin_injective h).

Русский

Если Fin n = Fin m, то cast h = Fin.cast (fin_injective h).

LaTeX

$$$\forall {n m}, \; (h : \mathrm{Fin}(n) = \mathrm{Fin}(m)) \Rightarrow \mathrm{cast}\,h = \mathrm{Fin.cast}(\mathrm{fin\_injective}\,h)$$$

Lean4

/-- A reversed version of `Fin.cast_eq_cast` that is easier to rewrite with. -/
theorem cast_eq_cast' {n m : ℕ} (h : Fin n = Fin m) : _root_.cast h = Fin.cast (fin_injective h) :=
  by
  cases fin_injective h
  rfl

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