Commit 2023-07-31 15:32 c8aaaf2c

View on Github →

feat(Order/Basic): simp lemmas about Subsingleton (#6092)

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Order/Basic.lean

added theorem le_of_subsingleton

added theorem not_lt_of_subsingleton