map_comp_apply — Mathlib

English

Evaluating map on a composition equals applying maps sequentially: map(g ∘ f)(x) = map g (map f(x)).

Русский

Оценка отображения на композицию равна последовательному применению отображений: map(g∘f)(x) = map g (map f(x)).

LaTeX

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

Lean4

theorem map_comp_apply (f : Hom P P') (g : Hom P' P'') (x) : CotangentSpace.map (g.comp f) x = .map g (.map f x) :=
  DFunLike.congr_fun (map_comp f g) x

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