mathlib3 documentation

order.filter.small_sets

The filter of small sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 s p t
theorem filter.eventually_small_sets' {α : Type u_1} {l : filter α} {p : set α Prop} (hp : ⦃s t : set α⦄, s t p t p 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
@[simp]
theorem filter.small_sets_top {α : Type u_1} :
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) :
theorem filter.tendsto.of_small_sets {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {s : α set β} {f : α β} (hs : filter.tendsto s la lb.small_sets) (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.small_sets 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_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