length_permutationsAux2 — Mathlib

English

The length of the second projection of permutationsAux2 equals the length of the tail ys for any f.

Русский

Длина второй компоненты permutationsAux2 равна длине хвоста ys для любого f.

LaTeX

$$$\forall {\alpha}, {\beta}, (t:\alpha) (ts:\ List\alpha) (ys:\ List\alpha) (f:\ List\alpha \to \beta),\; \mathrm{length}\; (permutationsAux2 t ts [] ys f).2 = \mathrm{length}\; ys$$$

Lean4

theorem length_permutationsAux2 (t : α) (ts : List α) (ys : List α) (f : List α → β) :
    length (permutationsAux2 t ts [] ys f).2 = length ys := by induction ys generalizing f <;> simp [*]

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