dist_map_zero_lt_of_semiconj — Mathlib

English

If f,g1,g2 satisfy a semiconjugacy h between f, g1, g2, then dist(g1(0), g2(0)) < 2.

Русский

Если существуют g1,g2 и полуприводящая отображение h между f, g1, g2, то dist(g1(0), g2(0)) < 2.

LaTeX

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

Lean4

theorem dist_map_zero_lt_of_semiconj {f g₁ g₂ : CircleDeg1Lift} (h : Function.Semiconj f g₁ g₂) :
    dist (g₁ 0) (g₂ 0) < 2 :=
  calc
    dist (g₁ 0) (g₂ 0) ≤ dist (g₁ 0) (f (g₁ 0) - f 0) + dist _ (g₂ 0) := dist_triangle _ _ _
    _ = dist (f 0 + g₁ 0) (f (g₁ 0)) + dist (g₂ 0 + f 0) (g₂ (f 0)) := by
      simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub, abs_sub_comm (g₂ (f 0))]
    _ < 1 + 1 := (add_lt_add (f.dist_map_map_zero_lt g₁) (g₂.dist_map_map_zero_lt f))
    _ = 2 := one_add_one_eq_two

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