AsLinearOrder

Stream: mathlib4

[Violeta Hernández]

Random question, but why does docs#AsLinearOrder exist? Surely the correct mechanism to create a linear order from a total partial order is to... just give the total field in LinearOrder?

[Kenny Lau]

image.png

:thinking:

[Violeta Hernández]

This comes from all the way back in Lean 3 #4037. Was used for two proofs about lattices, but is no longer used anywhere.

[Violeta Hernández]

Confusingly, the theorems it was used to prove were about... linearly ordered lattices?

[Violeta Hernández]

docs#le_sup_iff and docs#inf_le_iff are now just stated in terms of linear orders which is certainly the correct thing to do.

[Violeta Hernández]

Can we just deprecate this?

[Violeta Hernández]

#31013