Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC