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 fun 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 α) :
Filter (Set α)

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

Equations
  • l.smallSets = l.lift' Set.powerset
Instances For
    theorem Filter.smallSets_eq_generate {α : Type u_1} {f : Filter α} :
    f.smallSets = Filter.generate (Set.powerset '' f.sets)
    theorem Filter.bind_smallSets_gc {α : Type u_1} :
    GaloisConnection (fun (L : Filter (Set α)) => L.bind Filter.principal) Filter.smallSets
    theorem Filter.HasBasis.smallSets {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
    l.smallSets.HasBasis p fun (i : ι) => 𝒫 s i
    theorem Filter.hasBasis_smallSets {α : Type u_1} (l : Filter α) :
    l.smallSets.HasBasis (fun (t : Set α) => t l) Set.powerset
    theorem Filter.tendsto_smallSets_iff {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : αSet β} :
    Filter.Tendsto f la lb.smallSets tlb, ∀ᶠ (x : α) in la, f x t

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

    theorem Filter.eventually_smallSets {α : Type u_1} {l : Filter α} {p : Set αProp} :
    (∀ᶠ (s : Set α) in l.smallSets, p s) sl, ts, p t
    theorem Filter.eventually_smallSets' {α : Type u_1} {l : Filter α} {p : Set αProp} (hp : ∀ ⦃s t : Set α⦄, s tp tp s) :
    (∀ᶠ (s : Set α) in l.smallSets, p s) sl, p s
    theorem Filter.frequently_smallSets {α : Type u_1} {l : Filter α} {p : Set αProp} :
    (∃ᶠ (s : Set α) in l.smallSets, p s) tl, st, p s
    theorem Filter.frequently_smallSets_mem {α : Type u_1} (l : Filter α) :
    ∃ᶠ (s : Set α) in l.smallSets, s l
    @[simp]
    theorem Filter.tendsto_image_smallSets {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : αβ} :
    Filter.Tendsto (fun (x : Set α) => f '' x) la.smallSets lb.smallSets Filter.Tendsto f la lb
    theorem Filter.Tendsto.image_smallSets {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : αβ} :
    Filter.Tendsto f la lbFilter.Tendsto (fun (x : Set α) => f '' x) la.smallSets lb.smallSets

    Alias of the reverse direction of Filter.tendsto_image_smallSets.

    theorem Filter.HasAntitoneBasis.tendsto_smallSets {α : Type u_1} {l : Filter α} {ι : Type u_4} [Preorder ι] {s : ιSet α} (hl : l.HasAntitoneBasis s) :
    Filter.Tendsto s Filter.atTop l.smallSets
    theorem Filter.monotone_smallSets {α : Type u_1} :
    Monotone Filter.smallSets
    @[simp]
    theorem Filter.smallSets_bot {α : Type u_1} :
    .smallSets = pure
    @[simp]
    theorem Filter.smallSets_top {α : Type u_1} :
    .smallSets =
    @[simp]
    theorem Filter.smallSets_principal {α : Type u_1} (s : Set α) :
    theorem Filter.smallSets_comap_eq_comap_image {α : Type u_1} {β : Type u_2} (l : Filter β) (f : αβ) :
    (Filter.comap f l).smallSets = Filter.comap (Set.image f) l.smallSets
    theorem Filter.smallSets_comap {α : Type u_1} {β : Type u_2} (l : Filter β) (f : αβ) :
    (Filter.comap f l).smallSets = l.lift' (Set.powerset Set.preimage f)
    theorem Filter.comap_smallSets {α : Type u_1} {β : Type u_2} (l : Filter β) (f : αSet β) :
    Filter.comap f l.smallSets = l.lift' (Set.preimage f Set.powerset)
    theorem Filter.smallSets_iInf {α : Type u_1} {ι : Sort u_3} {f : ιFilter α} :
    (iInf f).smallSets = ⨅ (i : ι), (f i).smallSets
    theorem Filter.smallSets_inf {α : Type u_1} (l₁ : Filter α) (l₂ : Filter α) :
    (l₁ l₂).smallSets = l₁.smallSets l₂.smallSets
    instance Filter.smallSets_neBot {α : Type u_1} (l : Filter α) :
    l.smallSets.NeBot
    Equations
    • =
    theorem Filter.Tendsto.smallSets_mono {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s : αSet β} {t : αSet β} (ht : Filter.Tendsto t la lb.smallSets) (hst : ∀ᶠ (x : α) in la, s x t x) :
    Filter.Tendsto s la lb.smallSets
    theorem Filter.Tendsto.of_smallSets {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s : αSet β} {f : αβ} (hs : Filter.Tendsto s la lb.smallSets) (hf : ∀ᶠ (x : α) in la, f x s x) :

    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 : Filter α} {l' : Filter α} {p : αProp} :
    (∀ᶠ (s : Set α) in l.smallSets, ∀ᶠ (x : α) in l', x sp x) ∀ᶠ (x : α) in l l', p x
    @[simp]
    theorem Filter.eventually_smallSets_forall {α : Type u_1} {l : Filter α} {p : αProp} :
    (∀ᶠ (s : Set α) in l.smallSets, xs, p x) ∀ᶠ (x : α) in l, p x
    theorem Filter.Eventually.smallSets {α : Type u_1} {l : Filter α} {p : αProp} :
    (∀ᶠ (x : α) in l, p x)∀ᶠ (s : Set α) in l.smallSets, xs, p x

    Alias of the reverse direction of Filter.eventually_smallSets_forall.

    theorem Filter.Eventually.of_smallSets {α : Type u_1} {l : Filter α} {p : αProp} :
    (∀ᶠ (s : Set α) in l.smallSets, xs, p x)∀ᶠ (x : α) in l, p x

    Alias of the forward direction of Filter.eventually_smallSets_forall.

    @[simp]
    theorem Filter.eventually_smallSets_subset {α : Type u_1} {l : Filter α} {s : Set α} :
    (∀ᶠ (t : Set α) in l.smallSets, t s) s l