mapComp_eq — Mathlib

English

Mapping by a composite morphism equals composing the mappings: map(f ∘ g) = map(f) ∘ map(g).

Русский

Отображение по композиции равняется композиции отображений: map(f ∘ g) = map(f) ∘ map(g).

LaTeX

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

Lean4

/-- Mapping by the composite morphism `f ≫ g` is the same as mapping by `f` then by `g`. -/
theorem mapComp_eq {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) = (map f) ⋙ (map g) :=
  by
  fapply Functor.ext
  · simp [Over.map, Comma.mapRight]
  · intro U V k
    ext
    simp

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