mapRange_zero

Mathlib.Data.Finsupp.Defs

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

← MathLib Explorer

English

If f maps 0 to 0, then mapRange f hf applied to the zero function is the zero function.

Русский

Если f(0) = 0, то mapRange f hf примененное к нулевой функции даёт нулевую функцию.

LaTeX

$$mapRange f hf (0 : α →₀ M) = 0$$

Lean4

@[simp]
theorem mapRange_zero {f : M → N} {hf : f 0 = 0} : mapRange f hf (0 : α →₀ M) = 0 :=
  ext fun _ => by simp only [hf, zero_apply, mapRange_apply]

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

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

Разделы

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

Аффилиация

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