map_add

Mathlib.Data.List.Intervals

URI: https://scilib.ai/kg/mathlib#List.Ico.map_add

← MathLib Explorer

English

Shifting every element of Ico n m by k yields Ico (n+k) (m+k).

Русский

Сдвиг всех элементов Ico n m на k даёт Ico (n+k) (m+k).

LaTeX

$$$\operatorname{map}(k+\cdot)\bigl(\operatorname{Ico}(n,m)\bigr)=\operatorname{Ico}(n+k,m+k)$$$

Lean4

theorem map_add (n m k : ℕ) : (Ico n m).map (k + ·) = Ico (n + k) (m + k) := by
  rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]

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

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

Разделы

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

Аффилиация

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