nodup_permutations'Aux_of_notMem — Mathlib

English

If x is not contained in s, then permutations'Aux x s has no duplicates.

Русский

Если x не принадлежит s, то permutations'Aux x s не имеет повторов.

LaTeX

$$$\forall \{\alpha\}, \forall s:\\ List \alpha, \forall x:\\ \alpha,\ (x \notin s) \\rightarrow \, (permutations'Aux x s).Nodup$$

Lean4

theorem nodup_permutations'Aux_of_notMem (s : List α) (x : α) (hx : x ∉ s) : Nodup (permutations'Aux x s) := by
  induction s with
  | nil => simp
  | cons y s IH =>
    simp only [not_or, mem_cons] at hx
    simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]
    refine ⟨fun _ => Ne.symm hx.left, ?_⟩
    rw [nodup_map_iff]
    · exact IH hx.right
    · simp

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