ext — Mathlib

English

Two OneHoms are equal if they agree on every input; extensionality for OneHom.

Русский

Два отображения типа OneHom равны, если они совпадают на каждом входе; экстенсионность OneHom.

LaTeX

$$$$ \forall f,g: \text{OneHom } M N,\ (\forall x \in M,\ f(x) = g(x)) \Rightarrow f = g. $$$$

Lean4

@[to_additive (attr := ext)]
theorem ext [One M] [One N] ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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