commute_iff_commute

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

SemiconjBy f g1 g2 is equivalent to Semiconj f g1 g2 (under the underlying real-valued functions).

Русский

SemiconjBy f g1 g2 эквивалентно Semiconj f g1 g2 для соответствующих отображений на ℝ.

LaTeX

$$$\\text{SemiconjBy}(f,g_1,g_2) \\iff \\text{Semiconj}(f,g_1,g_2)$$$

Lean4

theorem commute_iff_commute {f g : CircleDeg1Lift} : Commute f g ↔ Function.Commute f g :=
  CircleDeg1Lift.ext_iff

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

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

Разделы

Аффилиация

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