mathlib documentation

order.filter.small_sets

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.

def filter.small_sets {α : Type u_1} (l : filter α) :
filter (set α)

The filter l.small_sets is the largest filter containing all powersets of members of l.

Equations
Instances for filter.small_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.eventually_small_sets {α : Type u_1} {l : filter α} {p : set α → Prop} :
(∀ᶠ (s : set α) in l.small_sets, p s) ∃ (s : set α) (H : s l), ∀ (t : set α), t sp t
theorem filter.eventually_small_sets' {α : Type u_1} {l : filter α} {p : set α → Prop} (hp : ∀ ⦃s t : set α⦄, s tp tp s) :
(∀ᶠ (s : set α) in l.small_sets, p s) ∃ (s : set α) (H : s l), p s
theorem filter.frequently_small_sets {α : Type u_1} {l : filter α} {p : set α → Prop} :
(∃ᶠ (s : set α) in l.small_sets, p s) ∀ (t : set α), t l(∃ (s : set α) (H : s t), p 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_bot {α : Type u_1} :
@[simp]
theorem filter.small_sets_top {α : Type u_1} :
@[simp]
theorem filter.small_sets_comap {α : Type u_1} {β : Type u_2} (l : filter β) (f : α → β) :
theorem filter.comap_small_sets {α : Type u_1} {β : Type u_2} (l : filter β) (f : α → set β) :
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]
def filter.small_sets_ne_bot {α : Type u_1} (l : filter α) :
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) :
@[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 sp 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 sp 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 sp 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 sp 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