get_map — Mathlib

English

Applying map to a composed object and then taking get yields the same as applying the componentwise maps to the underlying get.

Русский

После применения отображения к композиции и взятия деструктора получается результат, равный применению соответствующих отображений к базовой структуре.

LaTeX

$$$\operatorname{get}(\mathrm{map}(f)(x)) = \mathrm{map}_{i}\bigl( (\mathrm{G}_i)\mathrm{map} f \bigr)(\operatorname{get}(x)).$$$

Lean4

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

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