isComplement'_of_disjoint_and_mul_eq_univ

English

If H and K are subgroups with H ∩ K = {e} (i.e., disjoint) and HK = G, then H and K form a complement in G.

Русский

Если H и K — подпгруппы с H ∩ K = {e} и HK = G, тогда H и K образуют дополнение в G.

LaTeX

$$Disjoint(H,K) ∧ (HK = G) ⇒ IsComplement'(H,K)$$

Lean4

theorem isComplement'_of_disjoint_and_mul_eq_univ (h1 : Disjoint H K) (h2 : ↑H * ↑K = (Set.univ : Set G)) :
    IsComplement' H K := by
  refine ⟨mul_injective_of_disjoint h1, fun g => ?_⟩
  obtain ⟨h, hh, k, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g
  exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩

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