sublists_append — Mathlib

English

sublists (l1 ++ l2) equals (sublists l2) >>= (λ x, (sublists l1).map (x ++)).

Русский

sublists (l1 ++ l2) = (sublists l2) ∘= (λ x, (sublists l1).map (x ++)).

LaTeX

$$$\\text{sublists}(l_1 ++ l_2) = (\\text{sublists}(l_2)) >>= (\\\\lambda x. (\\text{sublists}(l_1)).map (\\\\cdot \\\\ ++ x))$$$

Lean4

theorem sublists_append (l₁ l₂ : List α) :
    sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x)) :=
  by
  simp only [sublists, foldr_append]
  induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]

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