ball_dynEntourage_mem_nhds — Mathlib

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)

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