English
Let F be a family of maps F_i: X → α indexed by ι, and let S ⊆ X with x0 ∈ S. The family restricted to S is equicontinuous at x0 if and only if F is equicontinuous at x0 when considered on S.
Русский
Пусть F — семейство отображений F_i: X → α, индексируемое по ι, и пусть S ⊆ X с x0 ∈ S. Тогда ограниченная на S семейство экконтинуально в точке x0 тогда и только тогда, когда экконтинуальность F на S равносильна экконтинуальности всей семьи в точке x0.
LaTeX
$$$$ \operatorname{EquicontinuousAt}(S\restriction F, x_0) \iff \operatorname{EquicontinuousWithinAt}(F, S, x_0). $$$$
Lean4
theorem equicontinuousAt_restrict_iff (F : ι → X → α) {S : Set X} (x₀ : S) :
EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S x₀ := by
simp [EquicontinuousWithinAt, EquicontinuousAt, ← eventually_nhds_subtype_iff]
