commutator_mono

Mathlib.GroupTheory.Commutator.Basic

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

← MathLib Explorer

English

If H1 ≤ K1 and H2 ≤ K2 then [H1, H2] ≤ [K1, K2].

Русский

Если H1 ⊆ K1 и H2 ⊆ K2, то [H1, H2] ⊆ [K1, K2].

LaTeX

$$$$ [H_1, H_2] \\le [K_1, K_2] \\quad\\text{whenever } H_1 \\le K_1 \\text{ and } H_2 \\le K_2. $$$$

Lean4

theorem commutator_mono (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
  commutator_le.mpr fun _g₁ hg₁ _g₂ hg₂ => commutator_mem_commutator (h₁ hg₁) (h₂ hg₂)

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

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

Разделы

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

Аффилиация

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