Rel versus Relation

Stream: mathlib4

[Wrenna Robson]

So we have the Relation namespace, as in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Relation.html, and the bundled version, Rel, in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Rel.html.

Why do we have the two different versions, and what's the reason to prefer one over the other?

[Yaël Dillies]

Rel is, as of two days ago, finding new uses in uniform space theory and cover/packing theory. I would wait a bit longer for time to tell

[Wrenna Robson]

Exciting.

[Wrenna Robson]

(Was wondering about its use in Concepts.)

[Wrenna Robson]

OOh we're finally geting some packing theory?!