mem_doubleCoset_of_not_disjoint — Mathlib

English

If HaK and HbK are not disjoint, then HaK = HbK.

Русский

Если HaK и HbK неразделимы (непересекаются), то HaK = HbK.

LaTeX

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

Lean4

theorem mem_doubleCoset_of_not_disjoint {H K : Subgroup G} {a b : G}
    (h : ¬Disjoint (doubleCoset a H K) (doubleCoset b H K)) : b ∈ doubleCoset a H K :=
  by
  rw [Set.not_disjoint_iff] at h
  simp only [mem_doubleCoset] at *
  obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h
  refine ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩
  rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]

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