English
If T is continuous, then for any U ∈ 𝓤 X and any n, the ball x around with radius dynEntourage(T,U,n) is a neighborhood of x.
Русский
Если T непрерывно, то для любого U ∈ 𝓤 X и любого n шар вокруг x с радиусом dynEntourage(T,U,n) является окрестностью x.
LaTeX
$$$\text{If } T \text{ is continuous and } U \in \mathcal{U}(X),\;\forall n,\; \mathrm{ball}(x, \mathrm{dynEntourage}(T,U,n)) \in \mathcal{N}(x).$$$
Lean4
theorem ball_dynEntourage_mem_nhds [UniformSpace X] {T : X → X} (h : Continuous T) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X)
(n : ℕ) (x : X) : ball x (dynEntourage T U n) ∈ 𝓝 x :=
by
rw [dynEntourage_eq_inter_Ico T U n, ball_iInter, Filter.iInter_mem, Subtype.forall]
intro k _
simp only [map_iterate, _root_.ball_preimage]
exact (h.iterate k).continuousAt.preimage_mem_nhds (ball_mem_nhds (T^[k] x) U_uni)