Commit 2025-08-24 17:49 34ba3725

View on Github →

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

Estimated changes

Modified Mathlib/Data/Finset/Option.lean

added theorem Finset.card_eraseNone_eq_card_erase

added theorem Finset.card_eraseNone_le

added theorem Finset.card_eraseNone_of_mem

added theorem Finset.card_eraseNone_of_not_mem