Theorem IsTotal.directed

Modification history

2026-01-20 13:02
Mathlib/Order/Directed.lean
chore(Order/Defs/Unbundled): deprecate `IsTotal` in favor of core's `Std.Total` (#33797)
Deleted IsTotal.directedView on Github →
2023-06-23 06:08
Mathlib/Order/Directed.lean
remove conditional completeness assumption in `IsCompact.exists_isMinOn` (#5388) …
Added IsTotal.directedView on Github →