Theorem IsTotal.directed

Modification history

2023-06-23 06:08
Mathlib/Order/Directed.lean
remove conditional completeness assumption in `IsCompact.exists_isMinOn` (#5388) …
Added IsTotal.directedView on Github →