## Stream: maths

### Topic: filter on sets

#### Yury G. Kudryashov (Jul 27 2020 at 20:28):

Is there a name for ⨅ s ∈ f, 𝓟 (powerset s) : filter (set α) where f : filter α?

#### Mario Carneiro (Jul 27 2020 at 20:30):

I don't think so, but I do think that this can be expressed as F powerset f for some F in mathlib

#### Yury G. Kudryashov (Jul 27 2020 at 20:32):

It can be useful to state, e.g., continuous_at f a → ∀ ε > 0, ∃ s ∈ nhds a, ∀ t ⊆ s, ∥∫ x in t, f x ∂μ - (μ t).to_real * f a∥ < ε * (μ t).to_real using is_o.

#### Mario Carneiro (Jul 27 2020 at 20:32):

F = filter.lift'

Last updated: May 12 2021 at 07:17 UTC