toTopologicalSpace_iInf — Mathlib

English

The topology of the infimum of a family equals the infimum of the topologies.

Русский

Топология инфимума семейства равномерных пространств равна инфимуму топологий.

LaTeX

$$(iInf u).toTopologicalSpace = iInf i (u i).toTopologicalSpace$$

Lean4

theorem toTopologicalSpace_iInf {ι : Sort*} {u : ι → UniformSpace α} :
    (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace :=
  TopologicalSpace.ext_nhds fun a ↦ by
    simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf, iInf_uniformity, @nhds_eq_comap_uniformity _ (u _),
      Filter.comap_iInf]

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