mapIso_hom_app — Mathlib

English

Componentwise, the hom component of the isomorphism mapIso f g h at an open U is the canonical equality induced by f = g.

Русский

Компонента гомоморфизма изоморфизма mapIso f g h в отношении открытого множества U равна каноническому равенству, вызываемому f = g.

LaTeX

$$$ (\mathrm{mapIso}(f,g,h)).\mathrm{hom}.\mathrm{app}}(U) = \mathrm{eqToHom}(\text{by }\mathrm{rw}(h)).$$$

Lean4

@[simp]
theorem mapIso_hom_app (f g : X ⟶ Y) (h : f = g) (U : Opens Y) : (mapIso f g h).hom.app U = eqToHom (by rw [h]) :=
  rfl

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