eqToIso_refl — Mathlib

English

For any X and any n, eqToIso h with h = rfl gives the identity isomorphism: X.eqToIso h = Iso.refl (X.obj (SimplexCategory.mk n)).

Русский

Для произвольного X и n, если h — тождественное равенство, то X.eqToIso h равно тождественному изоморфизму: Iso.refl (X.obj (SimplexCategory.mk n)).

LaTeX

$$$X.{\text{eqToIso}}(h) = \mathrm{Iso.refl}\,(X.obj(\text{SimplexCategory.mk } n))$ при $h = \mathrm{id}$$$

Lean4

@[simp]
theorem eqToIso_refl {n : ℕ} (h : n = n) : X.eqToIso h = Iso.refl _ := by simp [eqToIso]

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