dist_pow_map_zero_mul_translationNumber_le

English

For all f, n, the distance between (f^n)0 and n · τ f is bounded by 1: dist((f^n)0, n · f.translationNumber) ≤ 1.

Русский

Для каждого f, n расстояние dist((f^n)0, n · τ f) ограничено сверху единицей.

LaTeX

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

Lean4

theorem dist_pow_map_zero_mul_translationNumber_le (n : ℕ) : dist ((f ^ n) 0) (n * f.translationNumber) ≤ 1 :=
  f.translationNumber_pow n ▸ (f ^ n).dist_map_zero_translationNumber_le

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