The filter of small sets #
This file defines the filter of small sets w.r.t. a filter f
, which is the largest filter
containing all powersets of members of f
.
g
converges to f.small_sets
if for all s ∈ f
, eventually we have g x ⊆ s
.
An example usage is that if f : ι → E → ℝ
is a family of nonnegative functions with integral 1,
then saying that λ i, support (f i)
tendsto (𝓝 0).small_sets
is a way of saying that
f
tends to the Dirac delta distribution.
The filter l.small_sets
is the largest filter containing all powersets of members of l
.
Equations
- l.small_sets = l.lift' set.powerset
Instances for filter.small_sets
g
converges to f.small_sets
if for all s ∈ f
, eventually we have g x ⊆ s
.
Alias of the forward direction of filter.eventually_small_sets_forall`.
Alias of the reverse direction of filter.eventually_small_sets_forall`.