every type has a total order

Stream: mathlib4

[Enrico Borba]

Is there a proof that every type has a total order? I'm in the process of formalizing a logic textbook (for practice), and one of the consequences of the propositional compactness theorem is that every set has a total order.

I have a proof of it here, but I was curious if there this already exists in mathlib, or if a simpler proof, without developing all of the logic machinery, is possible. It's stated like this:

theorem total_preorder (M : Sort _) : ∃ r, IsTotalPreorder M r := ...

[Yaël Dillies]

docs#wellFoundedRel

[Enrico Borba]

lol

[Yaël Dillies]

Sorry, I meant docs#WellOrderingRel

[Enrico Borba]

Ahhh I see, okay thanks!