Zulip Chat Archive

Stream: general

Topic: filter docstrings


Johan Commelin (Mar 16 2022 at 06:51):

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 (Mar 16 2022 at 06:54):

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 (Mar 16 2022 at 06:54):

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

Mario Carneiro (Mar 16 2022 at 06:55):

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 (Mar 16 2022 at 06:56):

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

Mario Carneiro (Mar 16 2022 at 06:57):

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

Johan Commelin (Mar 16 2022 at 07:06):

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 (Mar 16 2022 at 07:12):

#12734 for the docstring of docs#filter.generate


Last updated: Dec 20 2023 at 11:08 UTC