semiconj — Mathlib

English

Let a ∈ G and b ∈ H be fixed. If the class AddConstMapClass F G H a b is given, then every map f ∈ F satisfies f(x + a) = f(x) + b for all x ∈ G.

Русский

Пусть фиксированы a ∈ G и b ∈ H. Пусть задан класс отображений AddConstMapClass F G H a b. Тогда для любого отображения f ∈ F и любого x ∈ G верно f(x + a) = f(x) + b.

LaTeX

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

Lean4

protected theorem semiconj [Add G] [Add H] [AddConstMapClass F G H a b] (f : F) : Semiconj f (· + a) (· + b) :=
  map_add_const f

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