dist_map_zero_translationNumber_le

English

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

Русский

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

LaTeX

$$$ \operatorname{dist}( f(0), τ(f) ) \le 1 $$$

Lean4

theorem dist_map_zero_translationNumber_le : dist (f 0) (τ f) ≤ 1 :=
  f.transnumAuxSeq_zero ▸
    dist_le_of_le_geometric_two_of_tendsto₀ (fun n => le_of_lt <| f.transnumAuxSeq_dist_lt n)
      f.tendsto_translationNumber_aux

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