filterMap_congr — Mathlib

English

If f and g are functions α → Option β such that f x = g x for all x ∈ l, then l.filterMap f = l.filterMap g.

Русский

Если для всех x ∈ l выполняется f x = g x, то l.filterMap f = l.filterMap g.

LaTeX

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

Lean4

theorem filterMap_congr {f g : α → Option β} {l : List α} (h : ∀ x ∈ l, f x = g x) : l.filterMap f = l.filterMap g := by
  induction l <;> simp_all [filterMap_cons]

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