English
If u : α → β is uniform inducing, then a family F is equicontinuous at x0 iff the composed family u ∘ F is equicontinuous at x0.
Русский
Если u : α → β — равномерно индуцирующее отображение, то семейство F экквинтино в точке x0 тогда и только тогда, когда u ∘ F экквинтино в x0.
LaTeX
$$$\\text{EquicontinuousAt } F x_0 \\iff \\text{EquicontinuousAt } (u \\circ F) x_0$ (under IsUniformInducing u).$$
Lean4
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is
equicontinuous at `x₀`. -/
theorem equicontinuousAt_iff {F : ι → X → α} {x₀ : X} {u : α → β} (hu : IsUniformInducing u) :
EquicontinuousAt F x₀ ↔ EquicontinuousAt ((u ∘ ·) ∘ F) x₀ :=
by
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]
rfl
