Theorem DirectedOn.is_bot_of_is_min

Modification history

2025-12-26 22:32
Mathlib/Order/Directed.lean
chore(Order/Directed): use `to_dual` (#32459) …
Deleted DirectedOn.is_bot_of_is_minView on Github →
2023-01-05 03:18
Mathlib/Order/Directed.lean
feat: synchronize with mathlib3 #17905 (#1280) …
Added DirectedOn.is_bot_of_is_minView on Github →