sublists'_eq_sublists'Aux — Mathlib

English

The auxiliary sublists operation satisfies a straightforward fold characterization: sublists'Aux a r1 r2 equals r2 concatenated with map (cons a) r1.

Русский

Вспомогательная операция sublists'Aux удовлетворяет равенству: sublists'Aux a r1 r2 = r2 ++ map (cons a) r1.

LaTeX

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

Lean4

theorem sublists'_eq_sublists'Aux (l : List α) : sublists' l = l.foldr (fun a r => sublists'Aux a r r) [[]] :=
  by
  simp only [sublists', sublists'Aux_eq_array_foldl]
  rw [← List.foldr_hom Array.toList]
  · intros; congr

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