isComplement'_bot_right

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.isComplement'_bot_right

English

IsComplement' H ⊥ is equivalent to H = ⊤.

Русский

IsComplement' H ⊥ эквивалентно H = ⊤.

LaTeX

$$$IsComplement'(H \\\\bot) \\\\Leftrightarrow H = \\\\top$$$

Lean4

@[to_additive (attr := simp)]
theorem isComplement'_bot_right : IsComplement' H ⊥ ↔ H = ⊤ :=
  isComplement_singleton_right.trans coe_eq_univ

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

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

Разделы

Аффилиация

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