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
theorem
filter.small_sets_eq_generate
{α : Type u_1}
{f : filter α} :
f.small_sets = filter.generate (set.powerset '' f.sets)
theorem
filter.has_basis.small_sets
{α : Type u_1}
{ι : Sort u_3}
{l : filter α}
{p : ι → Prop}
{s : ι → set α}
(h : l.has_basis p s) :
l.small_sets.has_basis p (λ (i : ι), 𝒫s i)
theorem
filter.has_basis_small_sets
{α : Type u_1}
(l : filter α) :
l.small_sets.has_basis (λ (t : set α), t ∈ l) set.powerset
theorem
filter.tendsto_small_sets_iff
{α : Type u_1}
{β : Type u_2}
{la : filter α}
{lb : filter β}
{f : α → set β} :
filter.tendsto f la lb.small_sets ↔ ∀ (t : set β), t ∈ lb → (∀ᶠ (x : α) in la, f x ⊆ t)
g
converges to f.small_sets
if for all s ∈ f
, eventually we have g x ⊆ s
.
theorem
filter.frequently_small_sets_mem
{α : Type u_1}
(l : filter α) :
∃ᶠ (s : set α) in l.small_sets, s ∈ l
theorem
filter.has_antitone_basis.tendsto_small_sets
{α : Type u_1}
{l : filter α}
{ι : Type u_2}
[preorder ι]
{s : ι → set α}
(hl : l.has_antitone_basis s) :
@[simp]
theorem
filter.small_sets_principal
{α : Type u_1}
(s : set α) :
(filter.principal s).small_sets = filter.principal (𝒫s)
theorem
filter.small_sets_comap
{α : Type u_1}
{β : Type u_2}
(l : filter β)
(f : α → β) :
(filter.comap f l).small_sets = l.lift' (set.powerset ∘ set.preimage f)
theorem
filter.comap_small_sets
{α : Type u_1}
{β : Type u_2}
(l : filter β)
(f : α → set β) :
filter.comap f l.small_sets = l.lift' (set.preimage f ∘ set.powerset)
theorem
filter.small_sets_infi
{α : Type u_1}
{ι : Sort u_3}
{f : ι → filter α} :
(infi f).small_sets = ⨅ (i : ι), (f i).small_sets
theorem
filter.small_sets_inf
{α : Type u_1}
(l₁ l₂ : filter α) :
(l₁ ⊓ l₂).small_sets = l₁.small_sets ⊓ l₂.small_sets
@[protected, instance]
theorem
filter.tendsto.small_sets_mono
{α : Type u_1}
{β : Type u_2}
{la : filter α}
{lb : filter β}
{s t : α → set β}
(ht : filter.tendsto t la lb.small_sets)
(hst : ∀ᶠ (x : α) in la, s x ⊆ t x) :
filter.tendsto s la lb.small_sets
@[simp]
theorem
filter.eventually_small_sets_eventually
{α : Type u_1}
{l l' : filter α}
{p : α → Prop} :
(∀ᶠ (s : set α) in l.small_sets, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
@[simp]
theorem
filter.eventually_small_sets_forall
{α : Type u_1}
{l : filter α}
{p : α → Prop} :
(∀ᶠ (s : set α) in l.small_sets, ∀ (x : α), x ∈ s → p x) ↔ ∀ᶠ (x : α) in l, p x
theorem
filter.eventually.of_small_sets
{α : Type u_1}
{l : filter α}
{p : α → Prop} :
(∀ᶠ (s : set α) in l.small_sets, ∀ (x : α), x ∈ s → p x) → (∀ᶠ (x : α) in l, p x)
Alias of the forward direction of filter.eventually_small_sets_forall
.
theorem
filter.eventually.small_sets
{α : Type u_1}
{l : filter α}
{p : α → Prop} :
(∀ᶠ (x : α) in l, p x) → (∀ᶠ (s : set α) in l.small_sets, ∀ (x : α), x ∈ s → p x)
Alias of the reverse direction of filter.eventually_small_sets_forall
.
@[simp]
theorem
filter.eventually_small_sets_subset
{α : Type u_1}
{l : filter α}
{s : set α} :
(∀ᶠ (t : set α) in l.small_sets, t ⊆ s) ↔ s ∈ l