map_comp_map — Mathlib

English

For maps f: X → Y and g: Y → Z and a map i: U → V in Opens Z, the double preimage respects composition: (map (f ≫ g)).map i = (map f).map ((map g).map i).

Русский

Для отображений f: X→Y, g: Y→Z и стрелки i: U → V в Opens Z верно: (map (f ≫ g)).map i = (map f).map ((map g).map i).

LaTeX

$$$ (\\mathrm{map}(f\\circ g)).\\mathrm{map} i = (\\mathrm{map} f).\\mathrm{map}((\\mathrm{map} g).\\mathrm{map} i)$$$

Lean4

@[simp]
theorem map_comp_map (f : X ⟶ Y) (g : Y ⟶ Z) {U V} (i : U ⟶ V) : (map (f ≫ g)).map i = (map f).map ((map g).map i) :=
  rfl

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