continuousOn_of_equicontinuousOn — Mathlib

English

If a family F: X → α tends to f pointwise on S and is equicontinuous on S, then f is continuous on S.

Русский

Если F: X → α сходится по точкам к f на S и эконтинуально на S, то f непрерывна на S.

LaTeX

$$$\forall x\in S, Tendsto (F·x) l (\mathcal{N}(f x)) \land EquicontinuousOn F S \Rightarrow ContinuousOn f S$$$

Lean4

/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S : Set X`* along some nontrivial
filter, and if the family `𝓕` is equicontinuous, then the limit is continuous on `S`. -/
theorem continuousOn_of_equicontinuousOn {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} {S : Set X}
    (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x))) (h₂ : EquicontinuousOn F S) : ContinuousOn f S := fun x hx ↦
  Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt h₁ (h₁ x hx) (h₂ x hx)

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