sublistsAux_eq_flatMap — Mathlib

English

sublistsAux equals r.flatMap (λ l, [l, a :: l]).

Русский

sublistsAux равно r.flatMap (λ l, [l, a :: l]).

LaTeX

$$$\\text{sublistsAux} = \\lambda a\\ r. r.flatMap (\\\\lambda l. [l, a :: l])$$$

Lean4

theorem sublistsAux_eq_flatMap : sublistsAux = fun (a : α) (r : List (List α)) => r.flatMap fun l => [l, a :: l] :=
  funext fun a =>
    funext fun r =>
      List.reverseRecOn r (by simp [sublistsAux])
        (fun r l ih => by
          rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]
          simp [sublistsAux])

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