## Stream: maths

### Topic: conditionally complete linear order for nnreal

#### Koundinya Vajjha (Jul 18 2019 at 16:49):

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 (Jul 18 2019 at 17:14):

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

#### Chris Hughes (Jul 18 2019 at 17:43):

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.

Last updated: May 14 2021 at 19:21 UTC