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



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.