continuous_of_mem — Mathlib

English

If H is a set of functions X → α that is equicontinuous, then any f ∈ H is a continuous function.

Русский

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

LaTeX

$$$f \\in H \\Rightarrow f \\in C(X, \\alpha)$$$

Lean4

protected theorem continuous_of_mem {H : Set <| X → α} (h : H.Equicontinuous) {f : X → α} (hf : f ∈ H) : Continuous f :=
  h.continuous ⟨f, hf⟩

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