dynEntourage_mem_uniformity — Mathlib

English

If T is uniformly continuous and U ∈ 𝓤 X, then the dynamical entourage dynEntourage T U n is also an entourage for every n.

Русский

Пусть T равномерно непрерывно, и U ∈ 𝓤 X. Тогда dynEntourage T U n принадлежит 𝓤 X для каждого n.

LaTeX

$$$\forall n,\; dynEntourage(T,U,n) \in \mathcal{U}(X)$ (при условии, что T равномерно непрерывно и U ∈ 𝓤 X).$$

Lean4

theorem dynEntourage_mem_uniformity [UniformSpace X] {T : X → X} (h : UniformContinuous T) {U : Set (X × X)}
    (U_uni : U ∈ 𝓤 X) (n : ℕ) : dynEntourage T U n ∈ 𝓤 X :=
  by
  rw [dynEntourage_eq_inter_Ico T U n]
  refine Filter.iInter_mem.2 fun k ↦ ?_
  rw [map_iterate T T k]
  exact uniformContinuous_def.1 (UniformContinuous.iterate T k h) U U_uni

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