instInfSet — Mathlib

English

InfSet (GroupTopology α) exists and collects infima over sets of group topologies.

Русский

Существует InfSet для GroupTopology α, задающее инфимы по множествам.

LaTeX

$$$\\mathrm{InfSet}(\\mathrm{GroupTopology}(\\alpha))$$$

Lean4

/-- Infimum of a collection of group topologies. -/
@[to_additive /-- Infimum of a collection of additive group topologies -/
    ]
instance : InfSet (GroupTopology α) where
  sInf S := ⟨sInf (toTopologicalSpace '' S), topologicalGroup_sInf <| forall_mem_image.2 fun t _ => t.2⟩

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