Commit 2023-01-23 07:49 1726f054

View on Github →

feat: port Data.Fintype.Order (#1718)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Order.lean

added theorem Directed.fintype_le

added theorem Fintype.bddAbove_range

added theorem Fintype.exists_le

added def Fintype.toBoundedOrder

added def Fintype.toOrderBot

added def Fintype.toOrderTop