Quantifier syntax for filters about mathlib HOT 6 CLOSED

Looks very good. I wondered if one should rather use the Isabelle order for parameters, i.e.,write
eventually (\lamba n, u n ≥0) at_top
or
eventually at_top (\lamba n, u n ≥0)
But in the end both are understandable even if one does not know that a filter is involved in the statement. And the second order, that you have chosen, makes it possible to also write at_top.eventually. So it is fine with me!

from mathlib.

The f.eventually notation is more flexible, both orders would work. I didn't use the Isabelle order, as it felt more natural to write the object we are operating on in the first position. Do you have a case were Isabelle's order has an advantage? In Isabelle most quantifiers over datatypes follow the form t_all : ('a -> bool) -> ('a t -> bool). I don't know if we have any precedence yet in mathlib.

Anyway, I hope that users don't directly write down eventually or frequently but use the quantifiers.

from mathlib.

If the user wants to use eventually, with Isabelle's order they have the advantage to choose between: f.eventually p or eventually p f. Unfortunately f.eventually itself does not work, it's missing the p.

I guess I will change it to Isabelle's order

from mathlib.

To me, the argument in favor of Isabelle order is that it looks more like a regular English sentence. But this is a weak argument.

from mathlib.

Added notation in #1845. Should we close this issue, or leave it to discuss what parts of the library should / should not be migrated to this notation?

from mathlib.

I think it's fine to close this now.

from mathlib.