isOpen

Mathlib.Topology.Algebra.OpenSubgroup

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

English

An open subgroup is open as a subset of G.

Русский

Открытая подгруппа является открытым подмножеством в G.

LaTeX

$$$\forall U \in \mathrm{OpenSubgroup}(G),\ (U: \mathrm{Set}G) \text{ is open in } G$$$

Lean4

@[to_additive]
protected theorem isOpen : IsOpen (U : Set G) :=
  U.isOpen'

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

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

Разделы

Аффилиация

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