arbitrary relations

Stream: mathlib4

[Anthony Bordg]

Consider an arbitrary relation $R \xhookrightarrow{} T\times S$ between a pair of sets (or classes) $T$ and $S$. I have the impression that the philosophy behind mathlib is to use types instead of sets, like this.

universe u v

variable {α : Type u} {β : Type v}

variable (R : α → β → Prop)

Is it correct?

[Ruben Van de Velde]

If I understand the question correctly, yes

[Anthony Bordg]

And then to talk about an element of the set or class of subsets of $T$, one directly consider an element I : Set α?

[Anthony Bordg]

Ruben Van de Velde said:

If I understand the question correctly, yes

Just to be clear, an alternative would be

universe u v

variable {α : Type u} {β : Type v} {T : Set α} {S : Set β}

variable (R : T → S → Prop)

and then to consider $I \subset T$ or $I \in \mathcal{P}(T)$, but I don't think it's the correct way to proceed in mathlib.

[Daniel Weber]

Note that the first approach is more general thanks to the coercion from Set to Type