The Coq mailing list

[Victor Porton <porton AT narod.ru>]

04.11.2011, 01:22, "Andrej Bauer" 
<andrej.bauer AT andrej.com>:
>> š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.)
>
> You coudl write for example as
>
> šššexists x, supremum S x /\ supremum T x

It is bad to introduce an extra variable.

> But if you have a lot of suprema and you work with complete posets,
> then it might be better to formalize complete posets with an actual
> operation "sup", so you could just write "sup S = sup T".

The trouble is that I work with arbitrary (non-complete) posets.

If I worked with complete posets only, there would be no problem.

-- 
Victor Porton - http://portonvictor.org