equicontinuousWithinAt_iff_left — Mathlib

English

If a single F is UniformEquicontinuous with respect to the k-th uniform structure u k, then it is UniformEquicontinuous with respect to the infimum of all u k.

Русский

Если F равномерно экквинтинустно относительно каждого u_k, то относительно infimum всех u_k.

LaTeX

$$$\\text{If } hk: \\operatorname{UniformEquicontinuous}(F) \\text{ w.r.t. } u_k \\text{ for all } k, \\text{ then } \\operatorname{UniformEquicontinuous}(F) \\text{ w.r.t. } \\inf_k u_k.$$$

Lean4

theorem equicontinuousWithinAt_iff_left {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {S : Set X} {x₀ : X}
    (hX : (𝓝[S] x₀).HasBasis p s) :
    EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U :=
  by
  rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
  rfl

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