English
A family F is EquicontinuousWithinAt F S x0 iff the swapped function is ContinuousWithinAt on S.
Русский
Эконтинуированность внутри S в x0 эквивалентна непрерывности перестановки внутри S.
LaTeX
$$$\\operatorname{EquicontinuousWithinAt} F S x_0 \\iff \\operatorname{ContinuousWithinAt} (\\text{ofFun} \\circ \\text{Function.swap } F : X \\to ^{\\!} \\iota \\to^{} α) S x_0.$$$
Lean4
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff the function
`swap 𝓕 : X → ι → α` is continuous at `x₀` within `S`
*when `ι → α` is equipped with the topology of uniform convergence*. This is very useful for
developing the equicontinuity API, but it should not be used directly for other purposes. -/
theorem equicontinuousWithinAt_iff_continuousWithinAt {F : ι → X → α} {S : Set X} {x₀ : X} :
EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) S x₀ :=
by
rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
rfl
