iterate — Mathlib

English

For any map T, the n-th iterate T^[n] is uniformly continuous if T is.

Русский

Для любого отображения T, если T равномерно непрерывна, то T^[n] равномерно непрерывна.

LaTeX

$$$ \text{UniformContinuous}^{(n)}(T) \text{ holds for all } n. $$$

Lean4

/-- If a function `T` is uniformly continuous in a uniform space `β`,
then its `n`-th iterate `T^[n]` is also uniformly continuous. -/
theorem iterate [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) : UniformContinuous T^[n] := by
  induction n with
  | zero => exact uniformContinuous_id
  | succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

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