map_mk — Mathlib

English

For f, the map of a composed element respects mk: mapping f over mk x equals mk of the componentwise maps.

Русский

При отображении f через композицию выполняется свойство: map f (mk x) = mk (map по компонентам x).

LaTeX

$$$\mathrm{map}\;\bigl(f\bigr)(\mathrm{Comp.mk}(x)) = \mathrm{Comp.mk}\bigl( \mathrm{inst.map} (\lambda i\; (\mathrm{G}_i)\mathrm{map} f\; x) \bigr).$$$

Lean4

theorem map_mk (x : F fun i ↦ G i α) : f <$$> Comp.mk x = Comp.mk ((fun i (x : G i α) ↦ f <$$> x) <$$> x) :=
  rfl

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