equicontinuous_restrict_iff — Mathlib

English

For a family F, equicontinuity of the restricted family to a subset S is equivalent to equicontinuity of the whole restricted to S.

Русский

Для семейства F равномерная эконтинуальность ограниченной семейство к подмножеству S эквивалентна равномерной эконтинуальности всей F на S.

LaTeX

$$$$ \operatorname{Equicontinuous}(S\restriction F) \iff \operatorname{EquicontinuousOn} F S. $$$$

Lean4

theorem equicontinuous_restrict_iff (F : ι → X → α) {S : Set X} :
    Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S := by
  simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff]

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