isInvariant_of_support_le — Mathlib

English

If a permutation c moves only elements inside a finite set s (i.e., c.support ⊆ s), then for every x, x ∈ s iff c(x) ∈ s.

Русский

Если перестановка c действует только внутри конечного множества s (c.support ⊆ s), то для любого x выполняется x ∈ s ⇔ c(x) ∈ s.

LaTeX

$$$c.\operatorname{support} \subseteq s \Rightarrow \forall x,\; c(x) \in s \leftrightarrow x \in s.$$$

Lean4

/-- The support of a permutation is invariant -/
theorem isInvariant_of_support_le {c : Perm α} {s : Finset α} (hcs : c.support ≤ s) (x : α) : c x ∈ s ↔ x ∈ s :=
  by
  by_cases hx' : x ∈ c.support
  · simp only [hcs hx', hcs (apply_mem_support.mpr hx')]
  · rw [notMem_support.mp hx']

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