equicontinuousOn — Mathlib

English

If a family F = {F_i} is equicontinuous on the whole space X, then it is equicontinuous on every subset S ⊆ X.

Русский

Если семейство функций F = {F_i} равномерно непрерывно на всей X, то оно равномерно непрерывно на любом подмножестве S ⊆ X.

LaTeX

$$$$ \operatorname{Equicontinuous} F \Rightarrow \operatorname{EquicontinuousOn} F S, \quad \text{for any } S \subseteq X. $$$$

Lean4

theorem equicontinuousOn {F : ι → X → α} (H : Equicontinuous F) (S : Set X) : EquicontinuousOn F S := fun x _ ↦
  (H x).equicontinuousWithinAt S

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