map_comp_obj — Mathlib

English

For a family of open sets U_i in Y, the mapped join equals the join of mapped opens: (map f).obj (iSup_i U_i) = iSup_i ((map f).obj U_i).

Русский

Для семейства открытых множеств U_i в Y совпадает отображение: (map f).obj (iSup_i U_i) = iSup_i ((map f).obj U_i).

LaTeX

$$$\\mathrm{map}_f(\\bigvee_i U_i) = \\bigvee_i (\\mathrm{map}_f)(U_i)$$$

Lean4

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

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