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.
```

Saw `finset.equivalence_partition`

, but that's not what's needed in this case, right?

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`

?

Oh.. yeah.. Thanks.

Dunno what I was thinking.

I'm taking only `y`

and I can't expect `x`

to be there always.

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