uniformContinuousOn_of_mem — Mathlib

English

If H is a set of functions that is uniformly equicontinuous on S, and f ∈ H, then f is uniformly continuous on S.

Русский

Если H — множество функций равномерно эквиконтинуально на S и f ∈ H, тогда f \\text{ равномерно непрерывна на } S.

LaTeX

$$$H.UniformEquicontinuousOn S \\Rightarrow \\forall f \\in H, UniformContinuousOn f S$$$

Lean4

protected theorem uniformContinuousOn_of_mem {H : Set <| β → α} {S : Set β} (h : H.UniformEquicontinuousOn S)
    {f : β → α} (hf : f ∈ H) : UniformContinuousOn f S :=
  h.uniformContinuousOn ⟨f, hf⟩

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