continuousWithinAt_of_mem — Mathlib

English

If H is equicontinuous within at S at x0, then any member restricted to S is continuous at x0 within S.

Русский

Если H равномерно внутри множества S в точке x0, то любой элемент, ограниченный множеством S, непрерывен в x0 внутри S.

LaTeX

$$$ \text{Set.EquicontinuousWithinAt.continuousWithinAt_of_mem} : \forall (H : Set (X \to \alpha)) (S : Set X) (x0 : X), H.EquicontinuousWithinAt S x0 \rightarrow \forall f \in H, \text{ContinuousWithinAt } f S x0 $$$

Lean4

protected theorem continuousWithinAt_of_mem {H : Set <| X → α} {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀)
    {f : X → α} (hf : f ∈ H) : ContinuousWithinAt f S x₀ :=
  h.continuousWithinAt ⟨f, hf⟩

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