eq_of_not_disjoint — Mathlib

English

The setoid on G defined by x ∼ y iff doubleCoset x H K = doubleCoset y H K is the same as the right/left quotient relation given by H.

Русский

Множество отношений на G, заданное x ∼ y тогда и только тогда, когда doubleCoset x H K = doubleCoset y H K, совпадает с обычной левой/правой факторной связью по H.

LaTeX

$$$ (setoid(\\uparrow H, \\uparrow K)).r = (QuotientGroup.leftRel H).r $$$

Lean4

theorem eq_of_not_disjoint {H K : Subgroup G} {a b : G} (h : ¬Disjoint (doubleCoset a H K) (doubleCoset b H K)) :
    doubleCoset a H K = doubleCoset b H K := by
  rw [disjoint_comm] at h
  have ha : a ∈ doubleCoset b H K := mem_doubleCoset_of_not_disjoint h
  apply doubleCoset_eq_of_mem ha

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