English
A family F: ι → X → α is equicontinuous at x0 iff the family of its range, viewed as a map from range F to X → α, is equicontinuous at x0.
Русский
Семейство F: ι → X → α эконтинуально в точке x0 тогда и только тогда, когда эконтinuально само множество функций из диапазона F в точке x0.
LaTeX
$$$\\operatorname{EquicontinuousAt} F x_0 \\iff \\operatorname{EquicontinuousAt} \\bigl((\\uparrow) : \\operatorname{range} F \\to X \\to \\alpha\\bigr) x_0.$$$
Lean4
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` iff `range 𝓕` is equicontinuous at `x₀`,
i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀`. -/
theorem equicontinuousAt_iff_range {F : ι → X → α} {x₀ : X} :
EquicontinuousAt F x₀ ↔ EquicontinuousAt ((↑) : range F → X → α) x₀ := by
simp only [EquicontinuousAt, forall_subtype_range_iff]
