Theorem Fintype.exists_le

Modification history

2024-01-16 04:25

Mathlib/Data/Fintype/Order.lean

chore(Fintype/Order): generalize Fintype to Finite in Directed lemmas (#9754)

Deleted Fintype.exists_le View on Github →

2023-08-10 19:52

Mathlib/Data/Fintype/Order.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Fintype.exists_le View on Github →

2023-01-23 07:49

Mathlib/Data/Fintype/Order.lean

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

Added Fintype.exists_le View on Github →