formPerm_apply_mem_ne_self_iff — Mathlib

English

For a Nodup l and x ∈ l, formPerm l x ≠ x iff 2 ≤ length l.

Русский

Для Nodup l и x ∈ l, formPerm l x ≠ x тогда и только тогда, когда 2 ≤ длина l.

LaTeX

$$$\forall {\alpha} [\DecidableEq \alpha],\ (l:\,\mathrm{List}\ \alpha),\ l.Nodup \rightarrow \forall x:\,\alpha,\ x \in l \rightarrow (formPerm l x \neq x) \\iff 2 \le l.length$$$

Lean4

theorem formPerm_apply_mem_ne_self_iff (hl : Nodup l) (x : α) (hx : x ∈ l) : formPerm l x ≠ x ↔ 2 ≤ l.length :=
  by
  rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]
  exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩

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