instSemilatticeInf

Mathlib.Topology.Algebra.Group.GroupTopology

URI: https://scilib.ai/kg/mathlib#GroupTopology.instSemilatticeInf

English

GroupTopologies form a meet-semilattice via the infimum operation.

Русский

Групповые топологии образуют полупорядованное по операции Inf.

LaTeX

$$$\\text{Min}(\\mathrm{GroupTopology}(\\alpha))$$$

Lean4

@[to_additive]
instance : SemilatticeInf (GroupTopology α) :=
  toTopologicalSpace_injective.semilatticeInf _ toTopologicalSpace_inf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru