Union of relations

Stream: Is there code for X?

[Eric Wieser]

Fabrizio Montesi said:

Giving an API and notation to Function.Rel (I want union, ... etc.)

Union is already there via r ⊔ s

[Fabrizio Montesi]

Eric Wieser said:

Union is already there via r ⊔ s

Where is it defined? It works but the docs is annoyingly not showing me any instances for Sup currently.

[Eric Wieser]

docs#Pi.sup_def is part of it

[Fabrizio Montesi]

Ah-ha! Thanks. And I see there's Inf as well.

[Eric Wieser]

docs#sup_Prop_eq is the other piece

[Fabrizio Montesi]

Skimming rapidly through it. IIUC, the latter file builds the expected lattice on Prop (and as join, or as meet), which can then be picked up by the former. Right?

[Fabrizio Montesi]

(Incidentially, order theory is one of the key reasons we depend on mathlib downstream in our research group. Great piece to have.)

[Notification Bot]

8 messages were moved here from #mathlib4 > Changing `Rel` to `Set (α × β)`, to help uniform spaces by Eric Wieser.