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



Am 11.04.2014 10:16, schrieb Christian Sternagel:
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.
Indeed.

btw: I could not find the constant "proj" in Equiv_Relations.
Oops, accidentally my answer referred to a development version (e.g. aff193f53a64), sorry for that. In Isabelle2013-2 this constant is in src/HOL/BNF/Equiv_Relations_More.

Dmitriy




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