set_support_apply_mem — Mathlib

English

For any permutation p and any a, p(a) is in the support of p if and only if a is in the support of p.

Русский

Для перестановки p и элемента a: p(a) принадлежит поддержке p тогда и только тогда, когда a принадлежит поддержке p.

LaTeX

$$$$ p(a) \in \{x \mid p(x) \neq x\} \iff a \in \{x \mid p(x) \neq x\}. $$$$

Lean4

theorem set_support_apply_mem {p : Perm α} {a : α} : p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x} := by simp

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