English
A family F: ι → X → α is EquicontinuousWithinAt F S x0 iff the range family is EquicontinuousWithinAt ((↑) : range F → X → α) S x0.
Русский
Аналогично локальной эконтинуированности: эконтинуированность внутри S в x0 равна эконтинуированности диапазона.
LaTeX
$$$\\operatorname{EquicontinuousWithinAt} F S x_0 \\iff \\operatorname{EquicontinuousWithinAt} \\bigl((\\uparrow) : \\operatorname{range} F \\to X \\to \\alpha\\bigr) S x_0.$$$
Lean4
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff `range 𝓕` is equicontinuous
at `x₀` within `S`, i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀` within `S`. -/
theorem equicontinuousWithinAt_iff_range {F : ι → X → α} {S : Set X} {x₀ : X} :
EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((↑) : range F → X → α) S x₀ := by
simp only [EquicontinuousWithinAt, forall_subtype_range_iff]
