translationNumber_conj_eq' — Mathlib

English

The distance between f^n(0) and n · τ f is at most 1: dist((f^n) 0, n τ f) ≤ 1.

Русский

Расстояние между f^n(0) и n · τ f не превосходит 1: dist((f^n)0, n τ f) ≤ 1.

LaTeX

$$$ \forall f \in CircleDeg1Lift, \forall n \in \mathbb{N}, \ dist((f^n)0, n \cdot τ f) \le 1. $$$

Lean4

@[simp]
theorem translationNumber_conj_eq' (f : CircleDeg1Liftˣ) (g : CircleDeg1Lift) : τ (↑f⁻¹ * g * f) = τ g :=
  translationNumber_conj_eq f⁻¹ g

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