map_natCast — Mathlib

English

For any f: α → β and any n ∈ ℕ, WithBot.map f (n : WithBot α) = f(n) in WithBot β.

Русский

Для любого f: α → β и любого n ∈ ℕ, WithBot.map f (n : WithBot α) = f(n) в WithBot β.

LaTeX

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

Lean4

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

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