ext_nat' — Mathlib

English

Let A be an AddZeroClass and F an AddMonoidHomClass from ℕ to A. If f(1) = g(1), then f = g.

Русский

Пусть A — добавочная нулевая структура, F — класс аддитивных гомоморфизмов ℕ в A. Если f(1) = g(1), то f = g.

LaTeX

$$$\forall A\,[\text{AddZeroClass } A]\,\forall F\,[\text{AddMonoidHomClass } F \mathbb{N} A],\ \forall f,g:F,\ f(1)=g(1) \Rightarrow f=g$$$

Lean4

theorem ext_nat' [AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
  DFunLike.ext f g <| by
    intro n
    induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn => simp [h, ihn]

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