mem_support_iff_of_commute — Mathlib

English

If g and c commute, then g preserves the support of c, i.e., g maps the support of c bijectively onto itself.

Русский

Если g и c коммутируют, то g сохраняет поддержку c, то есть отображает множество неподвижных точек c на себя (биективно).

LaTeX

$$$$ g c = c g \Rightarrow g( c\text{-support} ) = c\text{-support}. $$$$

Lean4

/-- If g and c commute, then g stabilizes the support of c -/
theorem mem_support_iff_of_commute {g c : Perm α} (hgc : Commute g c) (x : α) : g x ∈ c.support ↔ x ∈ c.support :=
  by
  simp only [mem_support, not_iff_not, ← mul_apply]
  rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]

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