doubleCoset_eq_of_mem — Mathlib

English

If doubleCosets HaK and HbK are not disjoint, then b ∈ HaK, hence HaK = HbK.

Русский

Если двойные косеты HaK и HbK не пересекаются, то b ∈ HaK, следовательно HaK = HbK.

LaTeX

$$$ \\lnot \\mathrm{Disjoint}(\\mathrm{doubleCoset}(a,H,K),\\ \\mathrm{doubleCoset}(b,H,K)) \\Rightarrow b \\in \\mathrm{doubleCoset}(a,H,K) $$$

Lean4

theorem doubleCoset_eq_of_mem {H K : Subgroup G} {a b : G} (hb : b ∈ doubleCoset a H K) :
    doubleCoset b H K = doubleCoset a H K :=
  by
  obtain ⟨h, hh, k, hk, rfl⟩ := mem_doubleCoset.1 hb
  rw [doubleCoset, doubleCoset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton, mul_assoc, mul_assoc,
    Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc, Subgroup.subgroup_mul_singleton hh]

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