LocallyFIniteOrderBot

Stream: mathlib4

[Sophie Morel]

Hi, I was trying to put an instance of LocallyFiniteOrderBot on some partially ordered set, so I decided to use LocallyFiniteOrderBot.ofIic. But then I realized that in mathlib4 (and in mathlib3), the theorem is called LocallyFiniteOrderTop.ofIic. I can still use it, of course, but I wonder whether this is a typo, as the name makes no sense.

[Sophie Morel]

@Yaël Dillies , since you're indicated as author of that file.

[Eric Wieser]

Yeah, docs4#LocallyFiniteOrderTop.ofIic looks like a typo

[Yaël Dillies]

Most likely a typo, yes