uniformContinuous_of_mem — Mathlib

English

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

Русский

Если H — множество функций и оно равномерно эквиконтинуально, то любой f ∈ H равномерно непрерывна.

LaTeX

$$$f \\in H \\Rightarrow UniformContinuous f$$$

Lean4

protected theorem uniformContinuous_of_mem {H : Set <| β → α} (h : H.UniformEquicontinuous) {f : β → α} (hf : f ∈ H) :
    UniformContinuous f :=
  h.uniformContinuous ⟨f, hf⟩

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