Theorem Finset.card_eraseNone_of_mem

Modification history

2025-08-24 17:49

Mathlib/Data/Finset/Option.lean

feat(Finset/Option): add lemmas about `#s.eraseNone` (#28839)

Added Finset.card_eraseNone_of_mem View on Github →