instTop

Mathlib.Topology.Algebra.OpenSubgroup

URI: https://scilib.ai/kg/mathlib#OpenSubgroup.instTop

English

There is a topology on OpenSubgroup G with top element ⊤ and isOpen_univ for it.

Русский

Существует топология на OpenSubgroup G, в которой верхний элемент — это ⊤ и открытое множество — все пространство.

LaTeX

$$$\text{Top}(\mathrm{OpenSubgroup}(G))$$$

Lean4

@[to_additive]
instance : Top (OpenSubgroup G) :=
  ⟨⟨⊤, isOpen_univ⟩⟩

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

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

Разделы

Аффилиация

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