# Documentation

Mathlib.Order.Filter.SmallSets

# 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.smallSets 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).smallSets is a way of saying that f tends to the Dirac delta distribution.

def Filter.smallSets {α : Type u_1} (l : ) :
Filter (Set α)

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

Equations
theorem Filter.smallSets_eq_generate {α : Type u_1} {f : } :
= Filter.generate (Set.powerset '' f.sets)
theorem Filter.HasBasis.smallSets {α : Type u_1} {ι : Sort u_2} {l : } {p : ιProp} {s : ιSet α} (h : ) :
Filter.HasBasis () p fun i => 𝒫 s i
theorem Filter.hasBasis_smallSets {α : Type u_1} (l : ) :
Filter.HasBasis () (fun t => t l) Set.powerset
theorem Filter.tendsto_smallSets_iff {α : Type u_2} {β : Type u_1} {la : } {lb : } {f : αSet β} :
Filter.Tendsto f la () ∀ (t : Set β), t lbFilter.Eventually (fun x => f x t) la

g converges to f.smallSets if for all s ∈ f, eventually we have g x ⊆ s.

theorem Filter.eventually_smallSets {α : Type u_1} {l : } {p : Set αProp} :
Filter.Eventually (fun s => p s) () s, s l ((t : Set α) → t sp t)
theorem Filter.eventually_small_sets' {α : Type u_1} {l : } {p : Set αProp} (hp : s t : Set α⦄ → s tp tp s) :
Filter.Eventually (fun s => p s) () s, s l p s
theorem Filter.frequently_smallSets {α : Type u_1} {l : } {p : Set αProp} :
Filter.Frequently (fun s => p s) () ∀ (t : Set α), t ls, s t p s
theorem Filter.frequently_smallSets_mem {α : Type u_1} (l : ) :
Filter.Frequently (fun s => s l) ()
theorem Filter.HasAntitoneBasis.tendsto_smallSets {α : Type u_2} {l : } {ι : Type u_1} [inst : ] {s : ιSet α} (hl : ) :
Filter.Tendsto s Filter.atTop ()
theorem Filter.monotone_smallSets {α : Type u_1} :
Monotone Filter.smallSets
@[simp]
theorem Filter.smallSets_bot {α : Type u_1} :
@[simp]
theorem Filter.smallSets_top {α : Type u_1} :
@[simp]
theorem Filter.smallSets_principal {α : Type u_1} (s : Set α) :
theorem Filter.smallSets_comap {α : Type u_2} {β : Type u_1} (l : ) (f : αβ) :
= Filter.lift' l (Set.powerset )
theorem Filter.comap_smallSets {α : Type u_2} {β : Type u_1} (l : ) (f : αSet β) :
= Filter.lift' l ( Set.powerset)
theorem Filter.smallSets_infᵢ {α : Type u_1} {ι : Sort u_2} {f : ι} :
= i, Filter.smallSets (f i)
theorem Filter.smallSets_inf {α : Type u_1} (l₁ : ) (l₂ : ) :
Filter.smallSets (l₁ l₂) =
instance Filter.smallSets_neBot {α : Type u_1} (l : ) :
Equations
theorem Filter.Tendsto.smallSets_mono {α : Type u_2} {β : Type u_1} {la : } {lb : } {s : αSet β} {t : αSet β} (ht : Filter.Tendsto t la ()) (hst : Filter.Eventually (fun x => s x t x) la) :
theorem Filter.Tendsto.of_smallSets {α : Type u_2} {β : Type u_1} {la : } {lb : } {s : αSet β} {f : αβ} (hs : Filter.Tendsto s la ()) (hf : Filter.Eventually (fun x => f x s x) la) :

Generalized squeeze theorem (also known as sandwich theorem). If s : α → Set β is a family of sets that tends to Filter.smallSets lb along la and f : α → β is a function such that f x ∈ s x eventually along la, then f tends to lb along la.

If s x is the closed interval [g x, h x] for some functions g, h that tend to the same limit 𝓝 y, then we obtain the standard squeeze theorem, see tendsto_of_tendsto_of_tendsto_of_le_of_le'.

@[simp]
theorem Filter.eventually_smallSets_eventually {α : Type u_1} {l : } {l' : } {p : αProp} :
Filter.Eventually (fun s => Filter.Eventually (fun x => x sp x) l') () Filter.Eventually (fun x => p x) (l l')
@[simp]
theorem Filter.eventually_smallSets_forall {α : Type u_1} {l : } {p : αProp} :
Filter.Eventually (fun s => (x : α) → x sp x) () Filter.Eventually (fun x => p x) l
theorem Filter.Eventually.smallSets {α : Type u_1} {l : } {p : αProp} :
Filter.Eventually (fun x => p x) lFilter.Eventually (fun s => (x : α) → x sp x) ()

Alias of the reverse direction of Filter.eventually_smallSets_forall.

theorem Filter.Eventually.of_smallSets {α : Type u_1} {l : } {p : αProp} :
Filter.Eventually (fun s => (x : α) → x sp x) ()Filter.Eventually (fun x => p x) l

Alias of the forward direction of Filter.eventually_smallSets_forall.

@[simp]
theorem Filter.eventually_smallSets_subset {α : Type u_1} {l : } {s : Set α} :
Filter.Eventually (fun t => t s) () s l