doubleCoset_union_leftCoset — Mathlib

English

doubleCoset_union_leftCoset: HaK = ⋃_{h ∈ H} h a K.

Русский

HaK = ⋃_{h ∈ H} h a K.

LaTeX

$$$ H a K = \\bigcup_{h \\in H} h a K $$$

Lean4

theorem doubleCoset_union_leftCoset (H K : Subgroup G) (a : G) : ⋃ h : H, (h * a : G) • ↑K = doubleCoset a H K :=
  by
  ext x
  simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset]
  constructor
  · rintro ⟨y, h_h⟩
    refine ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, ?_⟩
    simp only [← mul_assoc, one_mul, mul_inv_cancel, mul_inv_cancel_right, InvMemClass.coe_inv]
  · rintro ⟨x, hx, y, hy, hxy⟩
    refine ⟨⟨x, hx⟩, ?_⟩
    simp only [hxy, ← mul_assoc, hy, one_mul, inv_mul_cancel, inv_mul_cancel_right]

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