toList_ne_singleton — Mathlib

English

For any p and x, and for any y, the list toList p x cannot be the singleton [y].

Русский

Для любых p и x, и любого y, toList p x не может равняться одиночному списку [y].

LaTeX

$$$$\forall {\alpha} [Fintype \alpha] [DecidableEq \alpha] (p : Equiv.Perm \alpha) (x : \alpha) (y : \alpha),\ toList\ p\ x \neq [y].$$$$

Lean4

theorem toList_ne_singleton (y : α) : toList p x ≠ [y] :=
  by
  intro H
  simpa [card_support_ne_one] using congr_arg length H

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