subgroupOf_self

Mathlib.Algebra.Group.Subgroup.Map

URI: https://scilib.ai/kg/mathlib#Subgroup.subgroupOf_self

English

For any H ≤ G, H.subgroupOf H = ⊤.

Русский

Для любой H ⊆ G выполняется H.subgroupOf H = ⊤.

LaTeX

$$$ H.\\mathrm{subgroupOf} H = \\top $$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupOf_self : H.subgroupOf H = ⊤ :=
  top_unique fun g _hg => g.2

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

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

Разделы

Аффилиация

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