English
Uniform-induced: equicontinuity on a subset S is preserved when replacing F by u ∘ F, uniformly on S.
Русский
При равномерном индуцировании: экквинтоентность на подмножестве S сохраняется при замене F на u ∘ F.
LaTeX
$$$\\operatorname{EquicontinuousOn} F S \\iff \\operatorname{EquicontinuousOn} ((u \\circ \\cdot) \\circ F) S.$$$
Lean4
/-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous
iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is uniformly
equicontinuous. -/
theorem uniformEquicontinuous_iff {F : ι → β → α} {u : α → γ} (hu : IsUniformInducing u) :
UniformEquicontinuous F ↔ UniformEquicontinuous ((u ∘ ·) ∘ F) :=
by
have := UniformFun.postcomp_isUniformInducing (α := ι) hu
simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff]
rfl
