(simp) normal forms for expressions about `Filter`s

Stream: mathlib4

[Yury G. Kudryashov]

There are quite a few predicates involving Filters that can be written in several ways and Mathlib uses all these ways without clear guidelines. It would be nice to decide which forms are preferred, either everywhere through the library or depending on a use case.

• membership: we use
  • s ∈ f / {x | p x} ∈ f
  • ∀ᶠ x in f, x ∈ s / ∀ᶠ x in f, p x
  • f ≤ 𝓟 s / f ≤ 𝓟 {x | p x}
• set equality along a filter; while for functions we consistently(?) use f =ᶠ[l] g, for sets we use
  • s =ᶠ[l] t, mostly in the measure theory part of the library, with l = ae μ;
  • μ (s ∆ t) = 0 (rarely, because symmDiff is a recent addition to the library)
  • 𝓝[s] x = 𝓝[t] x
  • s ∈ 𝓝[t] x and t ∈ 𝓝[s] x as two separate assumptions
• set inequality along a filter; similarly, we use
  • s ≤ᵐ[μ] t;
  • μ(t \ s) = 0;
  • 𝓝[s] x ≤ 𝓝[t] x;
  • t ∈ 𝓝[s] x.

Each way has its pros and cons but I think that consistency is better than the current "each def/theorem uses whatever its author likes more" approach.

[Eric Wieser]

I think your second bullet has a typo, it doesn't mention f

[Yaël Dillies]

Yury G. Kudryashov said:

• μ (s ∆ t) = 0 (rarely, because symmDiff is a recent addition to the library)

What? It was added in 2021!

[Yury G. Kudryashov]

And made its way to measure theory library in 2022 !3#16918

[Yaël Dillies]

I guess adoption is slow here, and even slower since Patrick scoped the notation...

[Patrick Massot]

This is a tricky question. The only one I really want to get rid of is s ∈ f/ {x | p x} ∈ f.

[Patrick Massot]

About your second list, I am not shocked that things are expressed differently in topology and measure theory.

[Yury G. Kudryashov]

Patrick Massot said:

This is a tricky question. The only one I really want to get rid of is s ∈ f/ {x | p x} ∈ f.

I can try to drop Membership (probably, deprecating it first) and migrate to Filter.Eventually.

[Yury G. Kudryashov]

But we'll need guidelines about Eventually vs ≤ principal _. I would use Eventually everywhere but I know that you @Patrick Massot prefer ≤ principal _ in some cases (e.g., in the definition of IsCompact).

[Patrick Massot]

This may be a bit too drastic.

[Patrick Massot]

And I remember I was so proud when I managed to define that membership notation instead of using s ∈ f.sets. I think this was during the first Lean Together meeting. :older_man:

[Yury G. Kudryashov]

Then what do you suggest?

[Patrick Massot]

Not much, I think this is a difficult question.

[Patrick Massot]

I would like to see s ∈ f less often but still let people use it

[Yury G. Kudryashov]

I don't see a way to reduce usage of s ∈ f without deprecating (all lemmas about) it.

[Yury G. Kudryashov]

... and possibly replacing Filter.sets with Filter.Eventually.

[Jireh Loreaux]

I think migrating to Filter.Eventually for the first set is nice, but I also think it's fine to let people use membership or ≤ 𝓟

[Yury G. Kudryashov]

Patrick Massot said:

About your second list, I am not shocked that things are expressed differently in topology and measure theory.

AFAIR, I came up with this trick for measure theory. Topology&analysis had their conventions set up by then.