map_comp_obj_unop — Mathlib

English

For f: X → Y, g: Y → Z and open set U with a proof p, (map (f ≫ g)).obj ⟨U,p⟩ = (map f).obj ((map g).obj ⟨U,p⟩).

Русский

Для f: X→Y, g: Y→Z и открытого множества U с доказательством p выполняется (map (f ≫ g)).obj ⟨U,p⟩ = (map f).obj ((map g).obj ⟨U,p⟩).

LaTeX

$$$ (\\mathrm{map}(f\\circ g)).\\mathrm{obj} \\langle U,p\\rangle = (\\mathrm{map} f).\\mathrm{obj}((\\mathrm{map} g).\\mathrm{obj}\\langle U,p\\rangle)$$$

Lean4

@[simp]
theorem map_comp_obj_unop (f : X ⟶ Y) (g : Y ⟶ Z) (U) :
    (map (f ≫ g)).obj (unop U) = (map f).obj ((map g).obj (unop U)) :=
  rfl

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