sublists_map — Mathlib

English

The sublists of the map of f over l equals the map of f applied to the sublists of l.

Русский

Подсписки отображения map f на l равны отображению map f применённому к подспискам l.

LaTeX

$$$\\mathrm{sublists}(\\mathrm{map} f\, l) = \\mathrm{map}(\\mathrm{map} f)\\, (\\mathrm{sublists} l)$$$

Lean4

theorem sublists_map (f : α → β) : ∀ (l : List α), sublists (map f l) = map (map f) (sublists l)
  | [] => by simp
  | a :: l =>
    by
    rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons, bind_eq_flatMap, map_eq_flatMap,
      map_eq_flatMap]
    induction sublists l <;> simp [*]

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