mapIso_inv_app — Mathlib

English

Similarly, the inv component of mapIso f g h at U is the canonical equality induced by f = g.

Русский

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

LaTeX

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

Lean4

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

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