instInhabited

Mathlib.Topology.Algebra.Group.GroupTopology

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

English

The infimum of a set of group topologies has as underlying space the infimum of the images of their topologies.

Русский

Инфинум множества топологий группы имеет основание, равное инфимума соответствующих топологий.

LaTeX

$$$(sInf s).toTopologicalSpace = sInf (toTopologicalSpace \\circ s)$$$

Lean4

@[to_additive]
instance : Inhabited (GroupTopology α) :=
  ⟨⊤⟩

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

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

Разделы

Аффилиация

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