toSubmonoid_strictMono

Mathlib.Algebra.Group.Subgroup.Defs

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

English

The map from subgroups to submonoids is strictly monotone.

Русский

Отображение подгрупп в подмонойды строго монотонно.

LaTeX

$$$\\text{StrictMono}(\\mathrm{toSubmonoid})$$$

Lean4

@[to_additive (attr := mono)]
theorem toSubmonoid_strictMono : StrictMono (toSubmonoid : Subgroup G → Submonoid G) := fun _ _ => id

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

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

Разделы

Аффилиация

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