flatMap_congr — Mathlib

English

If f x = g x for all x ∈ l, then l.flatMap f = l.flatMap g.

Русский

Если для каждого x ∈ l выполняется f x = g x, то l.flatMap f = l.flatMap g.

LaTeX

$$$\\\\forall {l:\\\\text{List }\\\\alpha} {f,g:\\\\alpha \\\\to \\\\beta},\\\\, (\\\\forall x \\\\in l, f x = g x) \\\\Rightarrow \\\\text{List.flatMap} f\ l = \\\\text{List.flatMap} g\ l.$$$

Lean4

theorem flatMap_congr {l : List α} {f g : α → List β} (h : ∀ x ∈ l, f x = g x) : l.flatMap f = l.flatMap g :=
  (congr_arg List.flatten <| map_congr_left h :)

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