map_some_eraseNone — Mathlib

English

The cardinality of eraseNone s equals the cardinality of s with none removed (s.erase none).

Русский

Кардинальность eraseNone s равна кардинальности s без none (s.erase none).

LaTeX

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

Lean4

@[simp]
theorem map_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    (eraseNone s).map Embedding.some = s.erase none := by rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]

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