union_quotToDoubleCoset — Mathlib

English

union_quotToDoubleCoset: the union over all q of quotToDoubleCoset(H,K,q) equals the entire group G.

Русский

объединение по всем q через quotToDoubleCoset(H,K,q) покрывает всю группу G.

LaTeX

$$$ \\bigcup_q \\mathrm{quotToDoubleCoset}(H,K,q) = G $$$

Lean4

theorem union_quotToDoubleCoset (H K : Subgroup G) : ⋃ q, quotToDoubleCoset H K q = Set.univ :=
  by
  ext x
  simp only [Set.mem_iUnion, quotToDoubleCoset, mem_doubleCoset, SetLike.mem_coe, Set.mem_univ, iff_true]
  use mk H K x
  obtain ⟨h, k, h3, h4, h5⟩ := mk_out_eq_mul H K x
  refine ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, ?_⟩
  simp only [h5, ← mul_assoc, one_mul, inv_mul_cancel, mul_inv_cancel_right]

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