Hi @sgouezel,

I was going through your theory and I had a couple of ideas:

• the bdd variants and liminf and limsup don't need to function parameter, this can be encoded using f.map u. We can still add notation for LIMSUP x ← f, u := (f.map u).limsup or similar. But the proofs get slightly shorter, as we avoid the function parameter.

• I added a filter.bounded r relation, where r is usually (≥) or (≤). This gives us a nice generalization and avoids some duplication. Instead of frequently_bdd I called it cobounded, but maybe there is a better name? I think we should also generalize bdd_above and bdd_below.

• I uses auto parameters like (hf : f.bounded (≥) . bounded_default) to avoid the duplication of some conditionally_complete_lattice to complete_lattice.

Here is my current development:
https://gist.github.com/johoelzl/497f2a880eda9b7143e8164e3cf2e8da

Thanks a lot for your comments. This is a very good remark that all the definitions only depend on the image of the filter under the map, and therefore that everything can be done directly in the filter language (and it gives more efficient proofs). Still, I am not sure I am willing to give up the interface in terms of functions, as it will be the way things will be used in applications (and many statements only make sense in this setting, for instance the fact that limsup (max u v) = max (limsup u) (limsup v), or the fact that limsup (u + v) \le limsup u + limsup v in reals or ennreals).

Would it be OK for you if I rename your limsup to filter_limsup, formulate all the proofs that can be done purely in filter language using filter_limsup, and then introduce a limsup for functions (not just a notation) and prove the additional properties that only make sense in this setting?

A side question: the auto parameter magic is very nice, but I am afraid that it will not play well with sledgehammer-like tools if/when they are available. Any thought about this?

I pushed no my version in bf04127 and e6264eb.

I split the file and moved the topological stuff to analysis/topology instead of imporing topology in the order directory.

@sgouezel I also complete removed the introduction of eventually. I think it would be good it you could open a separate PR or issue for it.

The name for the filter-only version is now Limsup and Liminf, for version with a function is now limsup and liminf, the upper-cases is now at least somehow related to Sup, Inf and supr, infi. I didn't add a copy of the theorems just instanced with f.map u. The more general versions should apply anyway. Maybe we need additional simp rules.

I don't think that the auto-parameters are problematic with something like Sledgehammer. The auto-param notation sould be just ignored and the statement itself can be easily solved by an ATP. I would not worry about how Sledghammer would behave without seeing it implemeted yet.