map_comp_apply — Mathlib

English

For a Cauchy sequence a, map I g (map I f a) equals map I (g ∘ f) a.

Русский

Для последовательности Коши a имеет место равенство: map I g (map I f a) = map I (g ∘ f) a.

LaTeX

$$$\mathrm{map}\ I\ g\big(\mathrm{map}\ I\ f\ a\big) = \mathrm{map}\ I\ (g \circ_\mathrm{L} f)\ a$$$

Lean4

theorem map_comp_apply (f : M →ₗ[R] N) (g : N →ₗ[R] P) (a : AdicCauchySequence I M) :
    map I g (map I f a) = map I (g ∘ₗ f) a :=
  rfl

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