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
Mario Carneiro (Jul 27 2020 at 20:32):
F = filter.lift'
Last updated: May 12 2021 at 07:17 UTC