map_comp_obj' — Mathlib

English

For continuous maps f: X → Y, g: Y → Z and an open U, the equality (map (f ≫ g)).obj ⟨U,p⟩ = (map f).obj ((map g).obj ⟨U,p⟩) holds.

Русский

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

LaTeX

$$$\\big(\\mathrm{map}(f\\circ g)\\big).\\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' (f : X ⟶ Y) (g : Y ⟶ Z) (U) (p) : (map (f ≫ g)).obj ⟨U, p⟩ = (map f).obj ((map g).obj ⟨U, p⟩) :=
  rfl

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