presheafToType_map — Mathlib

English

Restriction maps for presheafToType are given by precomposition with i.unop, i.e., (presheafToType X T).map i f = f ∘ i.unop.

Русский

Ограничение для presheafToType задаётся через предобщее композицию с i.unop: (presheafToType X T).map i f = f ∘ i.unop.

LaTeX

$$$(\\mathrm{presheafToType}\\ X\\ T).map i f = f \\circ i.unop$$$

Lean4

@[simp]
theorem presheafToType_map {T : Type*} {U V : (Opens X)ᵒᵖ} {i : U ⟶ V} {f} :
    (presheafToType X T).map i f = f ∘ i.unop :=
  rfl

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