two_le_length_toList_iff_mem_support

English

The list toList p x has length at least 2 exactly when x belongs to the support of p.

Русский

Список toList p x имеет длину не менее двух тогда и только тогда, когда x лежит в поддержке p.

LaTeX

$$$$2 \le \mathrm{length}(\mathrm{toList}\ p\ x) \iff x \in p\mathrm{.support}$$$$

Lean4

theorem two_le_length_toList_iff_mem_support {p : Perm α} {x : α} : 2 ≤ length (toList p x) ↔ x ∈ p.support := by simp

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