English
Equicontinuity of a family F is preserved under replacing each function by its composition with a fixed uniform-inducing map; equivalently, equicontinuity of F is equivalent to that of its image under u.
Русский
Экквинтоентность семейства сохраняется при замене каждой функции композициией с фиксированным равномерно индуцирующим отображением; то же самое эквивалентно экквинтоентности образа F под u.
LaTeX
$$$\\operatorname{Equicontinuous} F \\iff \\operatorname{Equicontinuous} ( (u \\circ \\cdot) \\circ F ).$$$
Lean4
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous iff the
family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is equicontinuous. -/
theorem equicontinuous_iff {F : ι → X → α} {u : α → β} (hu : IsUniformInducing u) :
Equicontinuous F ↔ Equicontinuous ((u ∘ ·) ∘ F) :=
by
congrm ∀ x, ?_
rw [hu.equicontinuousAt_iff]
