Theorem le_of_subsingleton

Modification history

2025-11-21 05:52

Mathlib/Order/Basic.lean

chore(Order/Basic): use `@[to_dual]` for `Preorder`/`PartialOrder` (#31852) …

Modified le_of_subsingleton View on Github →

2023-07-31 15:32

Mathlib/Order/Basic.lean

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

Added le_of_subsingleton View on Github →