presheaf_map_eqToHom_op — Mathlib

English

The presheaf map along eqToHom i on the opposite is equal to eqToHom (i ▸ rfl).

Русский

Отображение препришф по eqToHom i на противоположной стороне равно eqToHom (i ▸ rfl).

LaTeX

$$$X.presheaf.map (eqToHom i).op = eqToHom (i \\; \\triangleright \\; rfl)$$$

Lean4

theorem presheaf_map_eqToHom_op (X : Scheme) (U V : X.Opens) (i : U = V) :
    X.presheaf.map (eqToHom i).op = eqToHom (i ▸ rfl) := by rw [eqToHom_op, eqToHom_map]

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