sublists'Aux_eq_map — Mathlib

English

For any a and lists r1, r2, sublists'Aux a r1 r2 equals r2 followed by map (cons a) applied to r1.

Русский

Для любых a, r1, r2 выполняется равенство: sublists'Aux a r1 r2 = r2 ++ map (cons a) r1.

LaTeX

$$$\\mathrm{sublists'Aux}\\ a\\ r_1\\ r_2 = r_2 \\;++\\; \\mathrm{map} (\\mathrm{cons} \\, a)\\ r_1$$$

Lean4

theorem sublists'Aux_eq_map (a : α) (r₁ : List (List α)) :
    ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁ :=
  List.reverseRecOn r₁ (fun _ => by simp [sublists'Aux]) fun r₁ l ih r₂ =>
    by
    rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
    simp [sublists'Aux]

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