Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_total.directed

Modification history

2023-06-21 18:29

src/order/directed.lean

feat(topology/algebra/order/compact): remove conditional completeness assumption in `is_compact.exists_forall_le` (#18991)

Added is_total.directed View on Github →