The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

2011/11/3 Victor Porton <porton AT narod.ru>

But what if I want to write "supremum S == supremum T"? (to add more complexity, the first and the second supremum may be taken on different sets.)

How to write it in terms of "supremum S x" and "has_supremum"?

 

exists x, is_supremum S x /\ is_supremum T x.

Or, if you don't care about computability, prove the uniqueness of suprema, and then use constructive_definite_description (from the Description module) to build a function

supremum : forall S:Ensemble X, has_supremum S -> { x | is_supremum S x }.
--
Daniel Schepler