flatMap — Mathlib

English

If l is a list and for every a ∈ l, f a ~ g a, then l.flatMap f ~ l.flatMap g.

Русский

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

LaTeX

$$$l \\text{ is a list},\\forall a \\in l:\\ f(a) \\sim g(a) \\Longrightarrow l.flatMap f \\sim l.flatMap g$$$

Lean4

@[gcongr]
protected theorem flatMap {l₁ l₂ : List α} {f g : α → List β} (h : l₁ ~ l₂) (hfg : ∀ a ∈ l₁, f a ~ g a) :
    l₁.flatMap f ~ l₂.flatMap g :=
  .trans (.flatMap_left _ hfg) (h.flatMap_right _)

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