pi_ext — Mathlib

English

The equality of two linear maps f and g is equivalent to the pointwise equality on all Pi.single i x.

Русский

Согласование равенств f=g эквивалентно равенству на всех Pi.single i x по точкам.

LaTeX

$$$f = g \\iff \\forall i x, f(\\Pi.single i x) = g(\\Pi.single i x).$$$

Lean4

theorem pi_ext (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) : f = g :=
  toAddMonoidHom_injective <| AddMonoidHom.functions_ext _ _ _ h

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