toSubmonoid_le

Mathlib.Algebra.Group.Subgroup.Defs

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

English

p.toSubmonoid ≤ q.toSubmonoid iff p ≤ q.

Русский

p.toSubmonoid ≤ q.toSubmonoid тогда и только тогда, когда p ≤ q.

LaTeX

$$$p.toSubmonoid \\le q.toSubmonoid \\iff p \\le q$$$

Lean4

@[to_additive (attr := simp)]
theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q :=
  Iff.rfl

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

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

Разделы

Аффилиация

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