toList_eq_nil_iff — Mathlib

English

For every finite α and permutation p, toList p x is empty if and only if x is not moved by p.

Русский

Для каждой конечной α и перестановки p список toList p x пуст тогда и только тогда, когда x не участвует в переносе p.

LaTeX

$$$$\forall \alpha\ [\mathrm{Fintype}\ \alpha]\ [\mathrm{DecidableEq}\ \alpha] (p : \mathrm{Perm}\ \alpha) (x : \alpha),\ toList\ p\ x = [] \iff x \notin p\mathrm{.support}.$$$$

Lean4

@[simp]
theorem toList_eq_nil_iff {p : Perm α} {x} : toList p x = [] ↔ x ∉ p.support := by simp [toList]

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