uniformEquicontinuousOn_iInf_rng — Mathlib

English

UniformEquicontinuousOn F S is equivalent to ∀ k, UniformEquicontinuousOn F S.

Русский

UniformEquicontinuousOn через iInf_rng эквивалентно компонентной версии.

LaTeX

$$$\\operatorname{UniformEquicontinuousOn} F S \\iff \\forall k, \\operatorname{UniformEquicontinuousOn} F S.$$$

Lean4

theorem uniformEquicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'} {S : Set β} :
    UniformEquicontinuousOn (uα := ⨅ k, u k) F S ↔ ∀ k, UniformEquicontinuousOn (uα := u k) F S :=
  by
  simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)]
  unfold UniformContinuousOn
  rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]

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