filter docstrings

Stream: general

[Johan Commelin]

docs#filter.generate says

generate g is the smallest filter containing the sets g

That should be the largest filter, right?

In general, I think I recall that mathlib uses an ordering of filters that is opposite to the convention in most other literature. Is this explained, motivated somewhere in the docs? I couldn't find it.

[Mario Carneiro]

I don't think there is a strong literature convention on this, because filter inequality is generally denoted using $\subseteq$ and there are no questions about what direction this goes

[Damiano Testa]

I was recently reading
https://leanprover-community.github.io/theories/topology.html
where the order is mentioned.

[Mario Carneiro]

I believe the reasoning behind the order is that it makes more sense if you treat filters as "convergence spaces"; more things converge in a filter which is larger in the order

[Mario Carneiro]

in a sense this is abstracting away from the "implementation detail" of filters as sets of sets

[Mario Carneiro]

I think it also makes more sense wrt ∀ᶠ x in l, p x

[Johan Commelin]

I certainly think that the mathlib convention makes sense. But it might be good to mention this in the module docstring of the file order/filter/basic as well.

[Johan Commelin]

#12734 for the docstring of docs#filter.generate