Where is EventuallyEq.finite_iInter?

Stream: Is there code for X?

[Terence Tao]

I needed the following basic fact about filters: if a finite collection of sets agree in the filter, then their intersections do also:

import Mathlib

theorem EventuallyEq.finite_iInter {ι : Type*} {α : Type u_2} {l : Filter α} (s: Finset ι) {E : ι → Set α} {F : ι → Set α}
(h : ∀ i ∈ s, E i =ᶠ[l] F i) : ⋂ i ∈ s, E i =ᶠ[l] ⋂ i ∈ s, F i := by
  unfold Filter.EventuallyEq Filter.Eventually at h ⊢
  simp at h ⊢
  rw [<-Filter.biInter_finset_mem] at h
  apply Filter.mem_of_superset h
  intro a ha
  simp at ha ⊢
  change a ∈ ⋂ i ∈ s, E i ↔ a ∈ ⋂ i ∈ s, F i
  simp
  change ∀ i ∈ s, a ∈ E i ↔ a ∈ F i at ha
  exact ball_congr ha

For some reason I was unable to find many useful methods in the Filter library to prove this, though the countable version docs#EventuallyEq.countable_iInter of this fact exists for CountableInterFilter. I was able to prove it eventually, but I wonder if I was missing some obvious tool in MathLib to do this more easily?

[Yury G. Kudryashov]

Usage of =ᶠ[l] for sets is kind of a hack (we silently interpret s : Set α as α → Prop), and probably lacks some supporting lemmas.

[Yury G. Kudryashov]

AFAIR, I introduced this hack some time ago. I'm thinking about a better way of doing it; I'm going to try some over the holidays.

[Yury G. Kudryashov]

I'll post a golfed proof in ~10min

[Patrick Massot]

The expected statement is ∀ᶠ x in l, x ∈ ⋂ i ∈ s, E i ↔ x ∈ ⋂ i ∈ s, F i.

[Terence Tao]

Patrick Massot said:

The expected statement is ∀ᶠ x in l, x ∈ ⋂ i ∈ s, E i ↔ x ∈ ⋂ i ∈ s, F i.

The version above is what came out of applying measure_congr. What I really wanted to prove was

example {ι Ω : Type*} [MeasurableSpace Ω] (s: Finset ι) {E E' : ι → Set Ω} {μ: Measure Ω}
(h : ∀ i ∈ s, E' i =ᶠ[ae μ] E i) : μ (⋂ i ∈ s, E i) = μ (⋂ i ∈ s, E' i)

but the measure theory library was also lacking the tools I needed here.

[Yury G. Kudryashov]

For ae, you can use EventuallyEq.countable_iInter

[Yury G. Kudryashov]

I'm preparing a PR with all the finite versions.

[Terence Tao]

PR to Mathlib?

[Terence Tao]

Oh I remember now the (slight) problem with EventuallyEq.countable_iInter, it required ι to be Countable rather than s.

[Terence Tao]

I think I know how to get around this by using the coercions from s to ι but I thought it would be easier to search for a Finset version of this tool. (So maybe my MWE should actually be named EventuallyEq.finset_iInter.)

[Terence Tao]

In any case there is no urgency on my end since the previous code is a proof of the result, it just feels very non-golfed.

[Yury G. Kudryashov]

#9090

[Yury G. Kudryashov]

It has versions for finite ι and finite s (both as in Set.Finite and Finset). Also, it works for EventuallyLE and EventuallyEq.