hasCoeSubgroup

Mathlib.Topology.Algebra.OpenSubgroup

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

English

Every open subgroup U of G is a subgroup of G, via the natural inclusion.

Русский

Каждая открытая подгруппа U группы G является подгруппой G через естественное вложение.

LaTeX

$$$\forall U \in \mathrm{OpenSubgroup}(G),\ U \text{ is a subgroup of } G$$$

Lean4

@[to_additive]
instance hasCoeSubgroup : CoeTC (OpenSubgroup G) (Subgroup G) :=
  ⟨toSubgroup⟩

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

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

Разделы

Аффилиация

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