castOrderIso_toEquiv — Mathlib

English

The toEquiv component of castOrderIso corresponds to a standard Equiv.cast under the equality n = m.

Русский

Компонента toEquiv castOrderIso соответствует обычному Equiv.cast при равенстве n = m.

LaTeX

$$$\forall {n m : \mathbb{N}} (h : n = m), (castOrderIso h).toEquiv = Equiv.cast (h \ ▸ rfl)$$$

Lean4

/-- While in many cases `Fin.castOrderIso` is better than `Equiv.cast`/`cast`, sometimes we want to
apply a generic lemma about `cast`. -/
theorem castOrderIso_toEquiv (h : n = m) : (castOrderIso h).toEquiv = Equiv.cast (h ▸ rfl) := by subst h; rfl

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