mem_permutations_of_perm_lemma — Mathlib

English

Given a condition H on is and l, if H implies l is obtained from ts ++ is or l ∈ permutationsAux is [], then l ∈ permutations is.

Русский

Для условия H на is и l, если H значит, что l можно получить как ts ++ is или l ∈ permutationsAux is [], тогда l ∈ permutations is.

LaTeX

$$$$H \Rightarrow (l \in permutations\ is)$$$$

Lean4

theorem mem_permutations_of_perm_lemma {is l : List α}
    (H : l ~ [] ++ is → (∃ (ts' : _) (_ : ts' ~ []), l = ts' ++ is) ∨ l ∈ permutationsAux is []) :
    l ~ is → l ∈ permutations is := by simpa [permutations, perm_nil] using H

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