English
Under a uniform inducing map u, equicontinuity at x0 is preserved under postcomposition with u—equicontinuity is equivalent before and after composing with u.
Русский
При наличии равномерно индуцирующего отображения u эквиконтинуальность в x0 сохраняется при посткомпозиции с u.
LaTeX
$$$\\operatorname{equicontinuousAt}(F,x_0) \\iff \\operatorname{equicontinuousAt}( (u \\circ \\cdot) \\circ F, x_0)$.$$
Lean4
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` within a subset `S : Set X` iff the family `𝓕'`, obtained by composing each function
of `𝓕` by `u`, is equicontinuous at `x₀` within `S`. -/
theorem equicontinuousWithinAt_iff {F : ι → X → α} {S : Set X} {x₀ : X} {u : α → β} (hu : IsUniformInducing u) :
EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((u ∘ ·) ∘ F) S x₀ :=
by
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff]
rfl
