comp — Mathlib

English

If T is uniformly continuous, then its n-th iterate T^[n] is uniformly continuous.

Русский

Если T равномерно непрерывна, то её n-я повторная итерация T^[n] также равномерно непрерывна.

LaTeX

$$$ \text{UniformContinuous}(T) \Rightarrow \text{UniformContinuous}(T^{[n]}). $$$

Lean4

nonrec theorem comp [UniformSpace β] [UniformSpace γ] {g : β → γ} {f : α → β} (hg : UniformContinuous g)
    (hf : UniformContinuous f) : UniformContinuous (g ∘ f) :=
  hg.comp hf

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