sublists_reverse — Mathlib

English

sublists (reverse l) equals map reverse (sublists' l).

Русский

sublists (reverse l) = map reverse (sublists' l).

LaTeX

$$$\\text{sublists}(\\text{reverse}(l)) = \\text{map}(\\text{reverse})\\bigl(\\text{sublists}'(l)\\bigr)$$$

Lean4

theorem sublists_reverse (l : List α) : sublists (reverse l) = map reverse (sublists' l) := by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton, bind_eq_flatMap,
      map_map, flatMap_cons, append_nil, flatMap_nil, Function.comp_def]

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