English
Uniform equicontinuity is preserved under postcomposition with a uniform-inducing map: F is UniformEquicontinuous iff u ∘ F is UniformEquicontinuous.
Русский
Условие равномерной экквинтоентности сохраняется после посткомпозиции с равномерно индуцирующим отображением.
LaTeX
$$$\\operatorname{UniformEquicontinuous} F \\iff \\operatorname{UniformEquicontinuous} ((u \\circ \\cdot) \\circ F).$$$
Lean4
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous on a
subset `S : Set X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is
equicontinuous on `S`. -/
theorem equicontinuousOn_iff {F : ι → X → α} {S : Set X} {u : α → β} (hu : IsUniformInducing u) :
EquicontinuousOn F S ↔ EquicontinuousOn ((u ∘ ·) ∘ F) S :=
by
congrm ∀ x ∈ S, ?_
rw [hu.equicontinuousWithinAt_iff]
