Liminf/Limsup naming

Stream: mathlib4

[Anatole Dedecker]

I think the current naming of docs#Filter.limsInf and docs#Filter.liminf is really weird (if you can't see why, I'm talking about the additional s before Inf). I guess this is to have some sort of consistency with sInf, but it's really weird since s refers to Set and we are talking about a filter. An argument could be made about using fInf since the liminf is the natural extension of sInf to filters (in the sense that the liminf of a principal filter is just the infimum of the set EDIT: you need the set to be nonempty...), but I'd say the easiest way to solve it would be to keep limInf and liminf. Any thoughts on that?

[Yaël Dillies]

Have you thought about iLiminf/sLiminf?

[Anatole Dedecker]

That would work, but that s still looks a bit off imo...

[Yury G. Kudryashov]

Another way is to get rid of limsInf and use liminf id when needed.