perm_of_mem_permutations — Mathlib

English

If l1 ∈ permutations l2, then l1 is a permutation of l2. More generally, if l1 ∈ permutations l2, then l1 ~ l2.

Русский

Если l1 принадлежит permutations l2, то l1 является перестановкой l2. В частности, l1 ∈ permutations l2 → l1 ~ l2.

LaTeX

$$$$l_1 \in permutations(l_2) \rightarrow l_1 \sim l_2$$$$

Lean4

theorem perm_of_mem_permutations {l₁ l₂ : List α} (h : l₁ ∈ permutations l₂) : l₁ ~ l₂ :=
  (eq_or_mem_of_mem_cons h).elim (fun e => e ▸ Perm.refl _) fun m => append_nil l₂ ▸ perm_of_mem_permutationsAux m

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