disjoint_out — Mathlib

English

disjoint_out: distinct quotient elements give disjoint double cosets: if a ≠ b, then Disjoint (doubleCoset a.out H K) (doubleCoset b.out H K).

Русский

при a ≠ b, двойные косеты по представителям a и b разной косеты непересекаются.

LaTeX

$$$ a \\neq b \\Rightarrow \\mathrm{Disjoint}(\\mathrm{doubleCoset}(\\mathrm{Quotient.out}(a))\,H\,K,\; \\mathrm{doubleCoset}(\\mathrm{Quotient.out}(b))\,H\,K) $$$

Lean4

theorem disjoint_out {H K : Subgroup G} {a b : Quotient H K} :
    a ≠ b → Disjoint (doubleCoset a.out H K) (doubleCoset b.out (H : Set G) K) :=
  by
  contrapose!
  intro h
  simpa [out_eq'] using mk_eq_of_doubleCoset_eq (eq_of_not_disjoint h)

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