translate_apply

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.translate_apply

English

The inverse of translation by x sends y to y−x, i.e., (translate by x)^{-1}(y) = y−x.

Русский

Обратная трансляция по x отправляет y в y−x: (translate by x)^{-1}(y) = y−x.

LaTeX

$$$\\forall x,y \\in \\mathbb{R},\\ (translate(\\text{ofAdd }x))^{-1}(y) = -x + y$$$

Lean4

@[simp]
theorem translate_apply (x y : ℝ) : translate (Multiplicative.ofAdd x) y = x + y :=
  rfl

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

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

Разделы

Аффилиация

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