conditionally complete linear order for nnreal

Stream: maths

[Koundinya Vajjha]

I needed to prove that Sup K \in K for a K : set nnreal. I searched through the library and found the lemma cSup_mem_of_is_closed. But I couldn't use it since nnreal is not an instance of conditionally_complete_linear_order? (It is an instance of conditionally_complete_linear_order_with_bot though).

Can this situation be salvaged?

[Koundinya Vajjha]

I guess if I remove the with_both condition it becomes a conditionally_complete_linear_order.

[Chris Hughes]

Write an instance, proving one from the other. The fields won't quite be identical, the linear order bot will omit conditions about sets that aren't bounded below, but the definition of Inf stays the same, which is what matters.

Strictly, I think complete_lattice should probably extend conditionally_complete_lattice.