disjoint

Mathlib.GroupTheory.Complement

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

English

Disjointness of H and K follows from IsComplement'.

Русский

Дисjointность H и K следует из IsComplement'.

LaTeX

$$IsComplement' H K → Disjoint H K$$

Lean4

theorem disjoint (h : IsComplement' H K) : Disjoint H K :=
  h.isCompl.disjoint

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

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

Разделы

Аффилиация

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