map_sub_const — Mathlib

English

For additive groups G and H and a fixed a ∈ G, b ∈ H, f(x - a) = f(x) - b for all x.

Русский

Пусть G и H — группы по сложению, фиксированы a ∈ G, b ∈ H. Тогда для любого f ∈ F: f(x - a) = f(x) - b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_sub_const [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) : f (x - a) = f x - b := by
  simpa using map_sub_nsmul f x 1

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