reduceOption_map — Mathlib

English

Reducing after mapping through an option map commutes with mapping the reduction.

Русский

Уменьшение после отображения через Option.map коммутирует с отображением после уменьшения.

LaTeX

$$$\operatorname{reduceOption}(\mathrm{map}(\mathrm{Option.map}(f), l)) = \mathrm{map}(f, \operatorname{reduceOption}(l))$$$

Lean4

@[simp]
theorem reduceOption_map {l : List (Option α)} {f : α → β} :
    reduceOption (map (Option.map f) l) = map f (reduceOption l) := by
  induction l with
  | nil => simp only [reduceOption_nil, map_nil]
  | cons hd tl hl => cases hd <;> simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl

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