Uniform spaces and relations as sets

Stream: mathlib4

[Yaël Dillies]

In #23181, I am moving the material in Topology.UniformSpace.Defs that's purely logic to a new file Topology.UniformSpace.Entourage. People complained that this wasn't really about entourages, but rather about generic relations on a type α, considered as Set (α × α).

[Yaël Dillies]

This made me think that actually we already had an API for relations, which is used in a few places, but not many, namely docs#Rel. Rel α β is a type synonym for α → β → Prop. This is different to how we use relations in uniform spaces, where instead we would want something like Rel α α := Set (α × α), ie α × α → Prop, ie uncurried.

[Yaël Dillies]

I don't think we want two APIs for relations (in fact until today I thought we wanted none), so I am hoping we can unify the uniform space-originated material with Rel. In the uniform space world, the uncurried approach is forced upon by docs#Filter, and in particular docs#uniformity which has type Filter (α × α). In the existing uses of Rel, I think we could go by with using Set (α × β) instead of α → β → Prop. It's just quite a bit of churn to switch from one to the other.

[Yaël Dillies]

Therefore I am thinking that we should redefine Rel α β := Set (α × β) and give notation for the corresponding relation α → β → Prop, maybe something like a ~[R] b? Alternatively, provide a FunLike (Rel α β) α (β → Prop) instance.

[Yaël Dillies]

What do @Damien Thomine, @Anatole Dedecker, @Patrick Massot think?

[Patrick Massot]

This was discussed many times before. In the uniform space setting we really want sets in α × α, not α → α → Prop. And calling it Rel would not convey this. On the other hand I don’t have any use of Rel so you can get rid of Rel is you don’t like the duplication.

[Yaël Dillies]

I think I landed on a nice design:

abbrev Rel (α β : Type*) := Set (α × β)

namespace Rel

notation:50 a:50 " ~[" R "] " b:50 => (a, b) ∈ R

[Yaël Dillies]

Patrick Massot said:

calling it Rel would not convey this

Sorry, I am calling it Rel, but I claim this is no worse than what we already have, namely docs#idRel, docs#compRel, docs#IsSymmetricRel