Commit 2023-01-16 09:19 9a79dea5

View on Github →

feat: port Data.Finset.Order (#1584)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Order.lean

added theorem Directed.finset_le

added theorem Finset.exists_le