## Stream: math-comp users

### Topic: Converting rel to set function

#### Julin Shaji (Apr 12 2024 at 06:40):

I have a relation R : rel T where T : finType.

So, R would be like T -> T -> bool, right?

I wish to use this R to make a function f: {set T} -> {set T} such
that for f X,

• x ∈ X -> ∀y ∈ T, R x y -> y ∈ f X

ie, f kind of 'gathers together' info from R.

Is this a good way of doing this and proving it correct?

From mathcomp Require Import all_ssreflect.

Section Foo.
Context {T: finType} (a b: T).
Context (R: rel T) (X: {set T}).

Definition funify := [set y | x in X, y in T & R x y].

Goal forall x y: T,
x \in X ->
y \in funify ->
R x y.
Proof.
move => x y.
rewrite /funify /=.
Abort.

Goal forall x y: T,
R x y ->
x \in X ->
y \in funify.
Proof.
rewrite /funify /= => x y.
Abort.
End Foo.


#### Julin Shaji (Apr 12 2024 at 10:08):

Saw finset.equivalence_partition, but that's not what's needed in this case, right?

#### Emilio Jesús Gallego Arias (Apr 18 2024 at 12:40):

Umm, I don't see how the first goal could be true. For example take R = eq , T = 2 and X = {1,2} , then funify X = {1,2}, however 1 \in X 2 \in funify, however R 1 2 = false ?

#### Julin Shaji (Apr 19 2024 at 10:53):

Oh.. yeah.. Thanks.
Dunno what I was thinking.

#### Julin Shaji (Apr 19 2024 at 10:53):

I'm taking only y and I can't expect x to be there always.

#### Emilio Jesús Gallego Arias (Apr 22 2024 at 11:50):

I get the feeling that you may be thinking about some relation R with some more particular properties, for example the relation could be functional, or surjective, etc...

Last updated: Jul 25 2024 at 15:02 UTC