mem_permutationsAux2' — Mathlib

English

A variant stating the same mem condition using id as the identity function.

Русский

Вариант с тем же условием принадлежности, используя id в качестве тождественной функции.

LaTeX

$$$\forall {t},{ts},{ys},{l}: List\;\alpha, l \in (permutationsAux2 t ts [] ys id).2 \iff \exists l_1 l_2, l_2 \neq [] \land ys = l_1 ++ l_2 \land l = l_1 ++ t :: l_2 ++ ts$$$

Lean4

theorem mem_permutationsAux2' {t : α} {ts : List α} {ys : List α} {l : List α} :
    l ∈ (permutationsAux2 t ts [] ys id).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts := by
  rw [show @id (List α) = ([] ++ ·) by funext _; rfl]; apply mem_permutationsAux2

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