English
If a family F is uniformly equicontinuous on a set S with respect to each uniform structure u_k, then it is uniformly equicontinuous on S with respect to the infimum uniform structure ⨅k, u_k.
Русский
Если семейство F равномерно экквинтинустно на множестве S относительно каждой структуры u_k, то оно удовлетворяет этим же условиям относительно infimum структуры ⨅k, u_k.
LaTeX
$$$\\text{If } hk: \\operatorname{UniformEquicontinuousOn}(F,S,u_k) \\text{ for all } k, \\text{ then } \\operatorname{UniformEquicontinuousOn}(F,S,\\inf_k u_k).$$$
Lean4
theorem uniformEquicontinuousOn_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α} {S : Set β'} {k : κ}
(hk : UniformEquicontinuousOn (uβ := u k) F S) : UniformEquicontinuousOn (uβ := ⨅ k, u k) F S :=
by
simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢
unfold UniformContinuousOn
rw [iInf_uniformity]
exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k
