English
A refinement of the swap-stabilizer relation under permutation action: the equivalence with swap commutes with membership test.
Русский
Уточнение для леммы о стабильности при перестановке: эквивалентность совместима с проверкой принадлежности.
LaTeX
$$$\\text{swap\_mem\_stabilizer} \\; {\\alpha} \\; [DecidableEq] \\; {S} {a} {b} : \\text{Equiv.swap } a b \\in \\mathrm{stabilizer}(\\mathrm{Perm}(\\alpha), S) \\leftrightarrow (a \\in S \\leftrightarrow b \\in S).$$$
Lean4
theorem swap_mem_stabilizer {α : Type*} [DecidableEq α] {S : Set α} {a b : α} :
Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S) :=
by
rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]
simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]
exact ⟨fun h ↦ by simpa [Iff.comm] using h a, by intros; split_ifs <;> simp [*]⟩
