map_ext — Mathlib

English

Equality of maps from AdicCompletion I M to a target can be checked by evaluating on mk I M a for all a.

Русский

Сравнение отображений из AdicCompletion I M в цель можно проверить по образам mk I M a для всех a.

LaTeX

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

Lean4

/-- Equality of maps out of an adic completion can be checked on Cauchy sequences. -/
theorem map_ext {N} {f g : AdicCompletion I M → N}
    (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

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