Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-06 18:15 0c54c57c

View on Github →

feat(data/set/equitable): A singleton is equitable (#10192) Prove set.subsingleton.equitable_on and set.equitable_on_singleton.

Estimated changes

modified theorem set.equitable_on_empty