mul_apply_eq_iff — Mathlib

English

If two permutations σ and τ have disjoint supports, then their product fixes a point a precisely when both σ and τ fix a.

Русский

Если две перестановки σ и τ имеют несоприкасающиеся множества точек перемещения, то произведение στ зафиксирует элемент a тогда и только тогда каждый из σ и τ фиксирует a.

LaTeX

$$$$ \text{Disjoint}(\sigma,\tau) \;\Rightarrow\; (\sigma\tau)(a)=a \;\Leftrightarrow\; (\sigma(a)=a \wedge \tau(a)=a). $$$$

Lean4

theorem mul_apply_eq_iff {σ τ : Perm α} (hστ : Disjoint σ τ) {a : α} : (σ * τ) a = a ↔ σ a = a ∧ τ a = a :=
  by
  refine ⟨fun h => ?_, fun h => by rw [mul_apply, h.2, h.1]⟩
  rcases hστ a with hσ | hτ
  · exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩
  · exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩

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