English
Let the family F : ι → X' → α be equicontinuous on a set S ⊆ X' with respect to each topology t_k on X'. Then F is equicontinuous on S with respect to the infimum topology ⨅k, t_k (the coarsest topology making all t_k continuous).
Русский
Пусть семейство F : ι → X' → α экквиспонотипично на множество S ⊆ X' относительно каждой топологии t_k на X'. Тогда F эквиконтинуально на S при инфимумной топологии ⨅k t_k (наименьшая топология, делающая все t_k непрерывными).
LaTeX
$$$\\text{If } hk: \\operatorname{EquicontinuousOn}(F,S,t_k) \\text{ for all } k, \\text{ then } \\operatorname{EquicontinuousOn}(F,S,\\inf_k t_k).$$$
Lean4
theorem equicontinuousOn_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α} {S : Set X'} {k : κ}
(hk : EquicontinuousOn (tX := t k) F S) : EquicontinuousOn (tX := ⨅ k, t k) F S := fun x hx ↦
equicontinuousWithinAt_iInf_dom (hk x hx)
