translationNumber_translate — Mathlib

English

For any x ∈ ℝ, translation by x has translation number x: τ( translate(x) ) = x.

Русский

Пусть x ∈ ℝ; сдвиг на x имеет число трансляции x: τ(translate(x)) = x.

LaTeX

$$$ τ( translate(x) ) = x $$$

Lean4

theorem translationNumber_translate (x : ℝ) : τ (translate <| Multiplicative.ofAdd x) = x :=
  translationNumber_eq_of_tendsto₀' _ <| by
    simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
      mul_div_cancel_left₀ (M₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]

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