continuousAt_of_mem — Mathlib

English

If H is a set of functions that is equicontinuous at x0, then any member f ∈ H is continuous at x0.

Русский

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

LaTeX

$$$ \text{Set.EquicontinuousAt.continuousAt_of_mem} : \forall (H : Set (X \to \alpha)) (x_0 : X), H.EquicontinuousAt x_0 \rightarrow \forall f \in H, \text{ContinuousAt } f x_0 $$$

Lean4

protected theorem continuousAt_of_mem {H : Set <| X → α} {x₀ : X} (h : H.EquicontinuousAt x₀) {f : X → α} (hf : f ∈ H) :
    ContinuousAt f x₀ :=
  h.continuousAt ⟨f, hf⟩

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