toTopologicalSpace_sInf — Mathlib

English

The topology of the sInf (infimum over a set of uniform spaces) equals the infimum of the corresponding topologies.

Русский

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

LaTeX

$$(sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace$$

Lean4

theorem toTopologicalSpace_sInf {s : Set (UniformSpace α)} :
    (sInf s).toTopologicalSpace = ⨅ i ∈ s, @UniformSpace.toTopologicalSpace α i :=
  by
  rw [sInf_eq_iInf]
  simp only [← toTopologicalSpace_iInf]

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