mapRange_single

Mathlib.Data.Finsupp.Single

URI: https://scilib.ai/kg/mathlib#Finsupp.mapRange_single

← MathLib Explorer

English

For ha: a ≠ a', erase a (f.update a' b) = update (erase a f) a' b.

Русский

Для ha: a ≠ a', erase a (f.update a' b) = update (erase a f) a' b.

LaTeX

$$erase a (f.update a' b) = update (erase a f) a' b$$

Lean4

@[simp]
theorem mapRange_single {f : M → N} {hf : f 0 = 0} {a : α} {b : M} : mapRange f hf (single a b) = single a (f b) :=
  ext fun a' => by classical simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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