map_comp — Mathlib

English

The map OnePoint.map respects composition: for functions f: Y → Z and g: X → Y, OnePoint.map(f ∘ g) = OnePoint.map f ∘ OnePoint.map g.

Русский

Карта OnePoint.map сохраняет композицию: для f: Y → Z и g: X → Y выполняется OnePoint.map(f ∘ g) = OnePoint.map f ∘ OnePoint.map g.

LaTeX

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

Lean4

theorem map_comp {Z : Type*} (f : Y → Z) (g : X → Y) : OnePoint.map (f ∘ g) = OnePoint.map f ∘ OnePoint.map g :=
  (Option.map_comp_map _ _).symm

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