rel_iff — Mathlib

English

rel_iff expresses the double coset relation: x ∼ y holds iff there exist h ∈ H and k ∈ K with y = h x k.

Русский

rel_iff выражает отношение двойного косета: x ∼ y тогда и только тогда, когда существуют h ∈ H и k ∈ K с y = h x k.

LaTeX

$$$ x \\sim_{H,K} y \\iff \\exists a \\in H, \\exists b \\in K, y = a x b $$$

Lean4

theorem rel_iff {H K : Subgroup G} {x y : G} : setoid (↑H) (↑K) x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b :=
  Iff.trans
    ⟨fun (hxy : doubleCoset x H K = doubleCoset y H K) => hxy ▸ mem_doubleCoset_self H K y, fun hxy =>
      (doubleCoset_eq_of_mem hxy).symm⟩
    mem_doubleCoset

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