Re: [isabelle] system of representatives of an equivalence relation



Are specific representatives actually needed? It might be better to use the equivalence classes themselves. That is the point of this construction.

--lcp

> On 11 Apr 2014, at 09:16, Christian Sternagel <c.sternagel at gmail.com> wrote:
> 
> Thanks Dimitriy,
> 
> That looks similar to the construction I'm currently using ;), i.e.,
> 
>  "repsys A R = {(SOME x. x ∈ X) | X. X ∈ A // R}"
> 
> I was hoping that some properties are already proved about it. E.g., that two non-equal elements of "repsys A R" are not in relation w.r.t. "R", "repsys A R" is a subset of "A", ...
> 
> But it should be easy to do anyway. Would this be interesting for anybody else?
> 
> cheers
> 
> chris
> 
> btw: I could not find the constant "proj" in Equiv_Relations.
> 
>> On 04/11/2014 10:07 AM, Dmitriy Traytel wrote:
>> Hi Chris,
>> 
>> Am 11.04.2014 09:49, schrieb Christian Sternagel:
>>> Dear fellow Isabellers,
>>> 
>>> I am wondering whether there is already a way in the Isabelle/HOL
>>> library (or the AFP, for that matter) to obtain a system of
>>> representatives (I'm not sure whether this is the correct term, in
>>> German it is called "Repräsentantensystem") for a given equivalence
>>> relation, i.e., a set containing one representative of each
>>> equivalence class?
>> 
>> Something like this: "(λX. SOME x. x ∈ X) ` Equiv_Relations.proj r `
>> Field r"
>> 
>> The function Equiv_Relations.proj gives you the (non-empty) equivalence
>> class of an element.
>> 
>> Dmitriy
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.