uniformity — Mathlib

English

The uniformity on the product space ∀ i, α i equals the infimum of comaps of the uniformities of each α i along the projection maps.

Русский

Унитерность произведения ∀ i, α i равна инфимуму комапов униформностей компонентов по проекционным отображениям.

LaTeX

$$$\mathcal{U}(\forall i, \alpha i) = \bigwedge_{i} \mathrm{comap}(\lambda a. (a.i, a.i)) \mathcal{U}(\alpha i)$$$

Lean4

theorem uniformity : 𝓤 (∀ i, α i) = ⨅ i : ι, (Filter.comap fun a => (a.1 i, a.2 i)) (𝓤 (α i)) :=
  iInf_uniformity

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