dist_map_zero_lt_of_semiconjBy

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

← MathLib Explorer

English

If h is SemiconjBy f g1 g2, then dist(g1(0), g2(0)) < 2.

Русский

Если h является SemiconjBy f g1 g2, то dist(g1(0), g2(0)) < 2.

LaTeX

$$$\SemiconjBy(f,g_1,g_2) \Rightarrow \operatorname{dist}(g_1(0), g_2(0)) < 2$$$

Lean4

theorem dist_map_zero_lt_of_semiconjBy {f g₁ g₂ : CircleDeg1Lift} (h : SemiconjBy f g₁ g₂) : dist (g₁ 0) (g₂ 0) < 2 :=
  dist_map_zero_lt_of_semiconj <| semiconjBy_iff_semiconj.1 h

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

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

Разделы

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

Аффилиация

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