eraseNone_map_some — Mathlib

English

Applying eraseNone after mapping each element to some yields the original finite set with none removed appropriately.

Русский

После отображения каждого элемента в some применение eraseNone возвращает исходное множество без none.

LaTeX

$$$(\\text{eraseNone}(s)).\\text{map} \\text{some} = s.\\text{erase} \\text{none}$$$

Lean4

@[simp]
theorem eraseNone_map_some (s : Finset α) : eraseNone (s.map Embedding.some) = s :=
  by
  ext
  simp

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