Commit 2025-11-04 20:26 00416cf0

View on Github →

feat(Set): helper lemmas about set cardinality (#29833) A few lemmas I needed in formalizing Dilworth's theorem and vertex covers.

Estimated changes

Modified Mathlib/Data/Set/Card.lean

added theorem Set.encard_diff

added theorem Set.encard_le_card

added theorem Set.encard_ne_zero_of_mem

added theorem Set.one_le_encard_insert

added theorem Set.one_le_ncard_insert