mapRange_zero

Mathlib.Data.DFinsupp.Defs

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

← MathLib Explorer

English

Applying mapRange to the zero DFinsupp yields zero: mapRange f hf (0) = 0.

Русский

Применение mapRange к нулевой функции DFinsupp даёт нуль: mapRange f hf (0) = 0.

LaTeX

$$$ \mathrm{DFinsupp.mapRange} f\, hf\, (0) = 0 $$$

Lean4

@[simp]
theorem mapRange_zero (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) : mapRange f hf (0 : Π₀ i, β₁ i) = 0 :=
  by
  ext
  simp only [mapRange_apply, coe_zero, Pi.zero_apply, hf]

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

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

Разделы

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

Аффилиация

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