formPerm_eq_one_iff — Mathlib

English

A list l has formPerm l = 1 exactly when length l ≤ 1.

Русский

Перестановка formPerm списка l равна единице тогда, когда длина l ≤ 1.

LaTeX

$$$\forall {\alpha} [\DecidableEq \alpha],\ (l:\,\mathrm{List}\ \alpha),\ l.Nodup \rightarrow (\mathrm{formPerm}\ l = 1 \iff \mathrm{length}\ l \le 1)$$$

Lean4

theorem formPerm_eq_one_iff (hl : Nodup l) : formPerm l = 1 ↔ l.length ≤ 1 :=
  by
  rcases l with - | ⟨hd, tl⟩
  · simp
  · rw [← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self]
    constructor
    · simp +contextual
    · intro h
      simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self, add_le_iff_nonpos_left, length,
        nonpos_iff_eq_zero, length_eq_zero_iff] at h
      simp [h]

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