doubleCoset_eq_image2 — Mathlib

English

For any a ∈ α and sets S,T ⊆ α, the doubleCoset a S T equals Set.image2 (λ x y => x * a * y) S T, i.e. { s a t | s ∈ S, t ∈ T }.

Русский

Для любых a ∈ α и подмножеств S, T ⊆ α верно, что двойной косет a S T равен Set.image2 (λ x y => x * a * y) S T, то есть { s a t | s ∈ S, t ∈ T }.

LaTeX

$$$ \\mathrm{doubleCoset}(a,S,T) = \\mathrm{Set.image2}(\\lambda x,y \\;=>\\; x \\cdot a \\cdot y)\\; S\\; T $$$

Lean4

theorem doubleCoset_eq_image2 (a : α) (s t : Set α) : doubleCoset a s t = Set.image2 (· * a * ·) s t := by
  simp_rw [doubleCoset, Set.mul_singleton, ← Set.image2_mul, Set.image2_image_left]

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