get_map — Mathlib

English

Applying a map to a constant and then taking get equals applying the map to the value after get.

Русский

Применение отображения к константе и последующее извлечение значения эквивалентно применению отображения к значению после извлечения.

LaTeX

$$$\mathrm{get}\bigl(\mathrm{MvFunctor.map}\;f\; (\mathrm{Const.mk}(x))\bigr) = \mathrm{MvFunctor.map}\;f\; (\mathrm{Const.get}(\mathrm{Const.mk}(x))).$$$

Lean4

theorem get_map (x : (Const n A) α) : Const.get (f <$$> x) = Const.get x :=
  rfl

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