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.

source
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
source
theorem filter.small_sets_eq_generate {α : Type u_1} {f : filter α} :
f.small_sets = filter.generate (set.powerset '' f.sets)
source
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)
source
theorem filter.has_basis_small_sets {α : Type u_1} (l : filter α) :
l.small_sets.has_basis (λ (t : set α), t ∈ l) set.powerset
source
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.

source
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
source
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
source
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)
source
theorem filter.frequently_small_sets_mem {α : Type u_1} (l : filter α) :
∃ᶠ (s : set α) in l.small_sets, s ∈ l
source
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) :
filter.tendsto s filter.at_top l.small_sets
source
theorem filter.monotone_small_sets {α : Type u_1} :
monotone filter.small_sets
source
@[simp]
theorem filter.small_sets_bot {α : Type u_1} :
⊥.small_sets = has_pure.pure ∅
source
@[simp]
theorem filter.small_sets_top {α : Type u_1} :
⊤.small_sets = ⊤
source
@[simp]
theorem filter.small_sets_principal {α : Type u_1} (s : set α) :
(filter.principal s).small_sets = filter.principal (𝒫s)
source
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)
source
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)
source
theorem filter.small_sets_infi {α : Type u_1} {ι : Sort u_3} {f : ι → filter α} :
(infi f).small_sets = ⨅ (i : ι), (f i).small_sets
source
theorem filter.small_sets_inf {α : Type u_1} (l₁ l₂ : filter α) :
(l₁ ⊓ l₂).small_sets = l₁.small_sets ⊓ l₂.small_sets
source
@[protected, instance]
def filter.small_sets_ne_bot {α : Type u_1} (l : filter α) :
l.small_sets.ne_bot
source
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
source
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) :
filter.tendsto f la lb

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'.

source
@[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
source
@[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
source
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.

source
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.

source
@[simp]
theorem filter.eventually_small_sets_subset {α : Type u_1} {l : filter α} {s : set α} :
(∀ᶠ (t : set α) in l.small_sets, t ⊆ s) ↔ s ∈ l