toTopologicalSpace_iInf — Mathlib

English

A second articulation of the iInf of a family of group topologies with respect to underlying topologies.

Русский

Второе формальное выражение iInf семейств топологий группы относительно их оснований.

LaTeX

$$$\\mathrm{congr\\_arg}\\; \\mathrm{sInf}\\; (range\\;\\mathrm{comp}\\; _ _).\\mathrm{symm}$$$

Lean4

@[to_additive (attr := simp)]
theorem toTopologicalSpace_iInf {ι} (s : ι → GroupTopology α) :
    (⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace :=
  congr_arg sInf (range_comp _ _).symm

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