image_some_eraseNone — Mathlib

English

The image of eraseNone under the mapping some equals the original set with none removed.

Русский

Образ eraseNone под отображением some равен исходному множеству без none.

LaTeX

$$$\\text{image}(\\text{Some})\\big(\\text{eraseNone}(s)\\big) = s \\setminus \\{\\text{none}\\}$$$

Lean4

@[simp]
theorem image_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    (eraseNone s).image some = s.erase none := by ext (_ | x) <;> simp

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