map_ofNat — Mathlib

English

For any f: α → β and any n with n ≥ 2, WithBot.map f (ofNat(n) : WithBot α) equals ofNat(f(n)) in WithBot β.

Русский

Для любого отображения f: α → β и любого n ≥ 2 отображение WithBot.map применяется к образованию nat(n) и равно образованию nat(f(n)) в WithBot β.

LaTeX

$$$\\forall \\alpha \\beta\\ [AddMonoidWithOne \\alpha] [AddMonoidWithOne \\beta] \\, (f : \\alpha \\to \\beta) \\, (n : \\mathbb{N})\\; [n. AtLeastTwo] \\, : \\, \\mathrm{WithBot.map}\\ f (\\mathrm{ofNat}(n) : \\mathrm{WithBot}\\ \\alpha) = \\mathrm{ofNat}(f(n))$$

Lean4

@[simp]
theorem map_ofNat {f : α → β} (n : ℕ) [n.AtLeastTwo] : WithBot.map f (ofNat(n) : WithBot α) = f ofNat(n) :=
  map_coe f n

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