map_comp_apply — Mathlib

English

Equality of the AdicCauchySequence.map under map and mk: map I f (mk I M a) = mk I N (AdicCauchySequence.map I f a).

Русский

Равенство отображений: map I f (mk I M a) = mk I N (AdicCauchySequence.map I f a).

LaTeX

$$$\mathrm{map}\ I\ f (\mathrm{AdicCompletion.mk}\ I\ M\ a) = \mathrm{AdicCompletion.mk}\ I\ N (\mathrm{AdicCauchySequence.map}\ I\ f\ a)$$$

Lean4

theorem map_comp_apply (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : AdicCompletion I M) :
    map I g (map I f x) = map I (g ∘ₗ f) x :=
  by
  change (map I g ∘ₗ map I f) x = map I (g ∘ₗ f) x
  rw [map_comp]

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