sublists_eq_sublistsFast — Mathlib

English

The standard sublists coincides with the fast variant: sublists = sublistsFast.

Русский

Стандартная операция sublists совпадает с быстрой версией: sublists = sublistsFast.

LaTeX

$$$\\text{@sublists} = \\text{@sublistsFast}$$$

Lean4

@[csimp]
theorem sublists_eq_sublistsFast : @sublists = @sublistsFast :=
  by
  ext α l : 2
  trans l.foldr sublistsAux [[]]
  · rw [sublistsAux_eq_flatMap, sublists]
  · simp only [sublistsFast, sublistsAux_eq_array_foldl]
    rw [← foldr_hom Array.toList]
    · intros; congr

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