Commit 2024-09-12 07:15 002afcff

View on Github →

feat: Small.{u} sets are closed under various operations (#11126) This PR adds lemmas showing that sets constructed by applying basic set operations to small sets are themselves small. We now have corresponding Small ↥s versions of almost all of the Finite ↥s instances in the Finite.Set namespace.

Estimated changes

Modified Mathlib/Logic/Small/Basic.lean

Modified Mathlib/Logic/Small/Set.lean

added theorem small_biInter

added theorem small_empty

added theorem small_iInter

added theorem small_pair

added theorem small_sInter

added theorem small_single

modified theorem small_subset