filterMap_some — Mathlib

English

filterMap some (with identity embedding) returns the original Finset: s.filterMap some (by simp) = s.

Русский

filterMap some с естественным внедрением возвращает исходное множество: s.filterMap some (by simp) = s.

LaTeX

$$$ s.filterMap\\text{ some } (\\text{by simp}) = s $$$

Lean4

@[simp]
theorem filterMap_some : s.filterMap some (by simp) = s :=
  ext fun _ => by simp only [mem_filterMap, Option.some.injEq, exists_eq_right]

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