codisjoint_subgroupOf_sup

Mathlib.Algebra.Group.Subgroup.Ker

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

← MathLib Explorer

English

Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)).

Русский

Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)).

LaTeX

$$Codisjoint (H.subgroupOf (H \\sqcup K)) (K.subgroupOf (H \\sqcup K))$$

Lean4

@[to_additive]
theorem codisjoint_subgroupOf_sup (H K : Subgroup G) : Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)) :=
  by
  rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self]
  exacts [le_sup_left, le_sup_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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