card_eraseNone_eq_card_erase — Mathlib

English

The cardinality in the eraseNone context matches the previous equality: #s.eraseNone = #(s.erase none).

Русский

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

LaTeX

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

Lean4

theorem card_eraseNone_eq_card_erase [DecidableEq (Option α)] (s : Finset (Option α)) :
    #s.eraseNone = #(s.erase none) := by rw [← card_map Function.Embedding.some, map_some_eraseNone]

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