map_comp — Mathlib

English

For any f : α → β and g : β → γ, map (g ∘ f) = (map g) ∘ (map f).

Русский

Для любых f : α → β и g : β → γ выполняется map (g ∘ f) = (map g) ∘ (map f).

LaTeX

$$$ \forall {\alpha \to \beta} {\beta \to \gamma} (f) (g),\; \operatorname{map}(g \circ f) = (\operatorname{map} g) \circ (\operatorname{map} f)$$$

Lean4

theorem map_comp {f : α → β} {g : β → γ} : map (g ∘ f) = (map g).comp (map f) :=
  Eq.symm <| lift_ext _ _ fun _ ↦ by simp [map]

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