map_mk — Mathlib

English

Same identity for mk and lifted Cauchy sequences in a different formulation.

Русский

Та же идентичность в другой формулировке для mk и последовательностей Коши.

LaTeX

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

Lean4

@[simp]
theorem map_mk (f : M →ₗ[R] N) (a : AdicCauchySequence I M) :
    map I f (AdicCompletion.mk I M a) = AdicCompletion.mk I N (AdicCauchySequence.map I f a) :=
  rfl

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