# Zulip Chat Archive

## 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