ext_nat'' — Mathlib

English

Two additive ring homomorphisms (or suitable maps) from ℕ to R are equal if they agree on all natural numbers.

Русский

Два аддитивных кольцевых отображения ℕ → R равны, если они совпадают на всех n ∈ ℕ.

LaTeX

$$$ f = g \quad\text{if } f(n) = g(n)\;\forall n \in \mathbb{N} $$$

Lean4

/-- If two `MonoidWithZeroHom`s agree on the positive naturals they are equal. -/
theorem ext_nat'' [ZeroHomClass F ℕ A] (f g : F) (h_pos : ∀ {n : ℕ}, 0 < n → f n = g n) : f = g :=
  by
  apply DFunLike.ext
  rintro (_ | n)
  · simp
  · exact h_pos n.succ_pos

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