Intersecting all sets in a filter

Stream: mathlib4

[Kevin Buzzard]

The notation for Set.sInter won't eat a filter directly:

import Mathlib.Order.Filter.Basic

open Filter
example (A : Set 𝓧) : ⋂₀ (𝓟 A) = A := sorry -- doesn't compile
example (A : Set 𝓧) : ⋂₀ (𝓟 A).sets = A := sorry -- works fine

Would it be desirable/possible to extend this notation so that it applied to filters and returned a set?

[Yaël Dillies]

docs#Filter.ker