English
A family F is UniformEquicontinuousOn F S iff the range family is UniformEquicontinuousOn ((↑) : range F → X → α) S.
Русский
Униформная эконтинуированность на S эквивалентна диапазону.
LaTeX
$$$\\operatorname{UniformEquicontinuousOn} F S \\iff \\operatorname{UniformEquicontinuousOn} \\bigl((\\uparrow) : \\operatorname{range} F \\to X \\to \\alpha\\bigr) S.$$$
Lean4
/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff `range 𝓕` is uniformly
equicontinuous on `S`, i.e the family `(↑) : range F → β → α` is uniformly equicontinuous on `S`. -/
theorem uniformEquicontinuousOn_iff_range {F : ι → β → α} {S : Set β} :
UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((↑) : range F → β → α) S :=
⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h => h.comp (rangeFactorization F)⟩
