English
UniformEquicontinuous F is equivalent to UniformContinuous (swap F) when the target uses the uniform convergence topology.
Русский
Равномерная эконтинуированность эквивалентна униформной непрерывности перестановки.
LaTeX
$$$\\operatorname{UniformEquicontinuous} F \\iff \\operatorname{UniformContinuous} (\\text{ofFun} \\circ \\text{Function.swap } F).$$$
Lean4
/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff the function
`swap 𝓕 : β → ι → α` is uniformly continuous on `S`
*when `ι → α` is equipped with the uniform structure of uniform convergence*. This is very useful
for developing the equicontinuity API, but it should not be used directly for other purposes. -/
theorem uniformEquicontinuousOn_iff_uniformContinuousOn {F : ι → β → α} {S : Set β} :
UniformEquicontinuousOn F S ↔ UniformContinuousOn (ofFun ∘ Function.swap F : β → ι →ᵤ α) S :=
by
rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
rfl
