ext_nat — Mathlib

English

If two monoid-with-zero homomorphisms from ℕ agree on all positive natural numbers, they are equal.

Русский

Если два гомоморфизма MonoidWithZeroHom ℕ → A совпадают на всех положительных натуральных числах, они равны.

LaTeX

$$$ f = g \text{ if } f(n) = g(n) \text{ for all } n>0$$$

Lean4

@[ext]
theorem ext_nat {f g : ℕ →*₀ A} : (∀ {n : ℕ}, 0 < n → f n = g n) → f = g :=
  ext_nat'' f g

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