map_natCast

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.map_natCast

English

Mapping commutes with natCast: map f on n as a WithTop element equals f(n) as a WithTop.

Русский

Переображение сохраняет natCast: map f (n : WithTop α) = f n.

LaTeX

$$$\\\\forall {f : α \\\\to β} (n : \\\\mathbb{N}), WithTop.map f (n : WithTop α) = f n$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru