Zulip Chat Archive

Stream: maths

Topic: conditionally complete linear order for nnreal


view this post on Zulip 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?

view this post on Zulip Koundinya Vajjha (Jul 18 2019 at 17:14):

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

view this post on Zulip 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