ext — Mathlib

English

Let f and g be additive group homomorphisms between seminormed additive groups. If f(x) = g(x) for every x in the domain, then f = g.

Русский

Пусть f и g — аддитивные гомоморфизмы между полугруппами с нормами. Если для каждого x из области определения выполняется f(x) = g(x), то f = g.

LaTeX

$$$\\forall f,g:\\ V_1 \\to V_2,\\; (\\forall x:\\ V_1,\\ f(x)=g(x)) \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext (H : ∀ x, f x = g x) : f = g :=
  coe_inj <| funext H

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