mapIso_refl — Mathlib

English

For any morphisms f,g and a proof h that f = g, the associated isomorphism mapIso f g h between open-set categories is the identity on map f.

Русский

Для любых морфизмов f,g и доказательства h того, что f = g, соответствующее изоморфизмное отображение mapIso f g h между категориями открытых множеств является тождественным на map f.

LaTeX

$$$\forall X,Y:\ TopCat, \forall f,g:\, X\to Y, \forall h:\ f=g,\; mapIso(f,g,h)=\mathrm{Iso.refl}(\mathrm{map}(f)).$$$

Lean4

@[simp]
theorem mapIso_refl (f : X ⟶ Y) (h) : mapIso f f h = Iso.refl (map _) :=
  rfl

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