coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Where is the set theory?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Victor Porton <porton AT narod.ru>
Cc: Coq <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Where is the set theory?
Date: Thu, 03 Nov 2011 17:22:48 -0400

Victor Porton wrote:

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"?

How about:
exists x, supremum S x /\ supremum T x

Re: [Coq-Club] Where is the set theory?, (continued)