English
Let α be a type with a uniform structure u1, and for each i in an index set I a uniform structure u2(i) on β. A function f: α → β is uniformly continuous from (α, u1) to (β, iInf u2) if and only if for every i ∈ I, f is uniformly continuous from (α, u1) to (β, u2(i)).
Русский
Пусть α — множество с равномерной структурой u1, и для каждого i из множества индексов I задана равномерность u2(i) на β. Тогда функция f: α → β равномерно непрерывна относительно (α, u1) к (β, inf_i u2(i)) тогда и только тогда, когда для каждого i ∈ I функция f равномерно непрерывна относительно (α, u1) к (β, u2(i)).
LaTeX
$$$$\\UniformContinuous_{u_1, \\inf_{i} u_2(i)} f \\ \\Longleftrightarrow\\ \\forall i,\\; \\UniformContinuous_{u_1, u_2(i)} f.$$$$
Lean4
theorem uniformContinuous_iInf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ : ι → UniformSpace β} :
UniformContinuous[u₁, iInf u₂] f ↔ ∀ i, UniformContinuous[u₁, u₂ i] f :=
by
delta UniformContinuous
rw [iInf_uniformity, tendsto_iInf]
