map_comp — Mathlib

English

Let X, Y, Z be finite sets and g: Y → Z, f: X → Y. The map induced by g ∘ f equals the composition of the maps induced by g and by f: map(g ∘ f) = (map g) ∘ (map f).

Русский

Пусть X, Y, Z конечные множества и данные функции g: Y → Z, f: X → Y. Индуцированное отображение по композиции g ∘ f равно композиции индуцированных отображений: map(g ∘ f) = (map g) ∘ (map f).

LaTeX

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

Lean4

theorem map_comp [Finite X] [Finite Y] [Finite Z] (g : Y → Z) (f : X → Y) :
    map (g.comp f) (M := M) = (map g).comp (map f) := by
  ext s
  simp [map, Finsupp.mapDomain_comp]

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