Is there already a theory in the AFP or elsewhere that deals with linear extensions of partial orders or topological sortings of a DAG ? Thanks!
The linear extension of partial orders is formalised in the entry Szpilrajn
Last updated: Sep 13 2025 at 08:22 UTC