sup_eq_top

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.IsComplement'.sup_eq_top

English

If a pair satisfies IsComplement', then their join is the top subgroup.

Русский

Если пара удовлетворяет IsComplement', их сумма равна верхней подгруппе.

LaTeX

$$IsComplement' H K → H ⊔ K = ⊤$$

Lean4

theorem sup_eq_top (h : IsComplement' H K) : H ⊔ K = ⊤ :=
  h.isCompl.sup_eq_top

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

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

Разделы

Аффилиация

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