doubleCoset_union_rightCoset — Mathlib

English

doubleCoset_union_rightCoset: HaK = ⋃_{k ∈ K} H a k.

Русский

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

LaTeX

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

Lean4

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

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