map_ext' — Mathlib

English

Another ext principle form: equality on mk images suffices to deduce equality of linear maps from AdicCompletion I M to N.

Русский

Еще одна форма экстенции: равенство на образах mk достаточно для вывода равенства линейных отображений.

LaTeX

$$$\forall f,g:\mathrm{AdicCompletion} I M \to N,\ (\forall a:\mathrm{AdicCauchySequence} I M,\ f(\mathrm{mk} I M a) = g(\mathrm mk I M a)) \Rightarrow f=g$$$

Lean4

/-- Equality of linear maps out of an adic completion can be checked on Cauchy sequences. -/
@[ext]
theorem map_ext' {f g : AdicCompletion I M →ₗ[AdicCompletion I R] T}
    (h : ∀ (a : AdicCauchySequence I M), f (AdicCompletion.mk I M a) = g (AdicCompletion.mk I M a)) : f = g :=
  by
  ext x
  apply induction_on I M x h

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