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



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.