map_const_add

Mathlib.Algebra.AddConstMap.Basic

URI: https://scilib.ai/kg/mathlib#AddConstMapClass.map_const_add

← MathLib Explorer

English

For f ∈ F, a ∈ G and b ∈ H, f(a + x) = f(x) + b for all x ∈ G, i.e., map_const_add.

Русский

Для любого f ∈ F, a ∈ G и b ∈ H верно f(a + x) = f(x) + b для всех x ∈ G.

LaTeX

$$$\\forall f \\in F,\\forall x \\in G:\\ f(a + x) = f(x) + b$$$

Lean4

@[scoped simp]
theorem map_const_add [AddCommMagma G] [Add H] [AddConstMapClass F G H a b] (f : F) (x : G) : f (a + x) = f x + b := by
  rw [add_comm, map_add_const]

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

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

Разделы

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

Аффилиация

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