map_natCast' — Mathlib

English

If a structure-preserving map f sends 1 to 1, then it fixes all OfNat.ofNat n for natural numbers n (under suitable hypotheses).

Русский

Если отображение f сохраняет структуру и отправляет 1 в 1, то оно фиксирует все OfNat.ofNat n для всех натуральных n (при соответствующих предположениях).

LaTeX

$$$ f(\operatorname{OfNat.ofNat}(n)) = \operatorname{OfNat.ofNat}(n) $ for all n (under hypotheses).$$

Lean4

theorem map_natCast' {A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) :
    ∀ n : ℕ, f n = n :=
  eq_natCast' ((f : A →+ B).comp <| Nat.castAddMonoidHom _) (by simpa)

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