iInf_uniformity — Mathlib

English

For any index set ι and a family u: ι → UniformSpace α, the uniformity of the infimum space equals the infimum of the uniformities: 𝓤[iInf u] = ⨅ i, 𝓤[u i].

Русский

Для множества индексов ι и семейства u: ι → UniformSpace α, униформность пространства iInf u равна инфимуму 𝓤[u i].

LaTeX

$$$\mathcal{U}[iInf\,u] = \bigwedge_{i} \mathcal{U}[u(i)]$$$

Lean4

theorem iInf_uniformity {ι : Sort*} {u : ι → UniformSpace α} : 𝓤[iInf u] = ⨅ i, 𝓤[u i] :=
  iInf_range

Похожие утверждения