Infimum of equivalence relations is an equivalence relation

Stream: Is there code for X?

[David Wärn]

Is there a lemma to the effect of "if R i are all equivalence relations, then so is R x y := forall i, R i x y"?

[Yakov Pechersky]

Overloaded R here with two different types

[Bhavik Mehta]

Yakov Pechersky said:

Overloaded R here with two different types

How so? R has type ι → α → α where ι is the indexing set so each R i is an equivalence relation on α

[Kevin Buzzard]

Equivalence relations are a complete lattice and this is Inf

[Yakov Pechersky]

Bhavik Mehta said:

Yakov Pechersky said:

Overloaded R here with two different types

How so? R has type ι → α → α where ι is the indexing set so each R i is an equivalence relation on α

Post was edited, one of the R was renamed T.

[Kevin Buzzard]

Zulip tip: with the desktop app you can click on the small grey EDITED and see the original post

[Patrick Massot]

It also appears in the menu