toTopologicalSpace_sInf — Mathlib

English

The indexed infimum of a family of group topologies has as underlying space the indexed infimum of their underlying topologies.

Русский

Инфинум по индексу семейства топологий группы имеет основание как инфимум оснований.

LaTeX

$$$(\\iInf i, s i).toTopologicalSpace = \\iInf i, (s i).toTopologicalSpace$$$

Lean4

@[to_additive (attr := simp)]
theorem toTopologicalSpace_sInf (s : Set (GroupTopology α)) :
    (sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s) :=
  rfl

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