Mathlib.Order.Filter.SmallSets

Filter.smallSets definition

(l : Filter α) : Filter (Set α)

Full source

/-- The filter `l.smallSets` is the largest filter containing all powersets of members of `l`. -/
def smallSets (l : Filter α) : Filter (Set α) :=
  l.lift' powerset

Filter of small sets with respect to a filter

Informal description

Given a filter `l` on a type `α`, the filter `l.smallSets` is defined as the largest filter containing all powersets of members of `l`. Specifically, a set of sets `g` converges to `l.smallSets` if for every set `s ∈ l`, eventually all sets in `g` are subsets of `s`. More formally, `l.smallSets` is constructed by lifting the powerset operation over `l`, i.e., `l.smallSets = l.lift' powerset`.

Filter.smallSets_eq_generate theorem

{f : Filter α} : f.smallSets = generate (powerset '' f.sets)

Full source

theorem smallSets_eq_generate {f : Filter α} : f.smallSets = generate (powersetpowerset '' f.sets) := by
  simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]

Small Sets Filter as Generated by Powersets of Filter Sets

Informal description

For any filter $f$ on a type $\alpha$, the filter of small sets with respect to $f$ is equal to the filter generated by the image of the powerset operation applied to the sets in $f$. In symbols: $$f.\text{smallSets} = \text{generate}(\mathcal{P}(f.\text{sets})).$$

Filter.bind_smallSets_gc theorem

: GaloisConnection (fun L : Filter (Set α) ↦ L.bind principal) smallSets

Full source

theorem bind_smallSets_gc :
    GaloisConnection (fun L : Filter (Set α) ↦ L.bind principal) smallSets := by
  intro L l
  simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff]
  rfl

Galois Connection Between Filter Binding and Small Sets

Informal description

The function that maps a filter $L$ on the power set of $\alpha$ to the filter $L.\text{bind principal}$ forms a Galois connection with the `smallSets` operation. Specifically, for any filter $L$ on $\text{Set } \alpha$ and any filter $l$ on $\alpha$, we have: $$ L.\text{bind principal} \leq l \quad \text{if and only if} \quad L \leq l.\text{smallSets}. $$

Filter.HasBasis.smallSets theorem

{p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) : HasBasis l.smallSets p fun i => 𝒫 s i

Full source

protected theorem HasBasis.smallSets {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
    HasBasis l.smallSets p fun i => 𝒫 s i :=
  h.lift' monotone_powerset

Basis of Small Sets Filter via Powersets

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$. Then the filter $l.\text{smallSets}$ of small sets with respect to $l$ has a basis consisting of the powersets $\mathcal{P}(s_i)$ indexed by the same predicate $p_i$.

Filter.hasBasis_smallSets theorem

(l : Filter α) : HasBasis l.smallSets (fun t : Set α => t ∈ l) powerset

Full source

theorem hasBasis_smallSets (l : Filter α) :
    HasBasis l.smallSets (fun t : Set α => t ∈ l) powerset :=
  l.basis_sets.smallSets

Basis Characterization of Small Sets Filter via Powersets

Informal description

For any filter $l$ on a type $\alpha$, the filter $l.\text{smallSets}$ has a basis consisting of the powersets $\mathcal{P}(t)$ for all sets $t \in l$. More precisely, a set of sets $S$ belongs to $l.\text{smallSets}$ if and only if there exists a set $t \in l$ such that $\mathcal{P}(t) \subseteq S$.

Filter.Eventually.exists_mem_basis_of_smallSets theorem

 {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ᶠ t in l.smallSets, P t) (h₂ : HasBasis l p s) :
  ∃ i, p i ∧ P (s i)

Full source

theorem Eventually.exists_mem_basis_of_smallSets {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop}
    (h₁ : ∀ᶠ t in l.smallSets, P t) (h₂ : HasBasis l p s) : ∃ i, p i ∧ P (s i) :=
  (h₂.smallSets.eventually_iff.mp h₁).imp fun _i ⟨hpi, hi⟩ ↦ ⟨hpi, hi Subset.rfl⟩

Existence of Basis Set Satisfying Eventual Property in Small Sets Filter

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$. If a property $P$ holds eventually in the small sets filter $l.\text{smallSets}$, then there exists an index $i$ such that $p_i$ holds and $P$ holds for the basis set $s_i$.

Filter.Frequently.smallSets_of_forall_mem_basis theorem

 {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ i, p i → P (s i)) (h₂ : HasBasis l p s) :
  ∃ᶠ t in l.smallSets, P t

Full source

theorem Frequently.smallSets_of_forall_mem_basis {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop}
    (h₁ : ∀ i, p i → P (s i)) (h₂ : HasBasis l p s) : ∃ᶠ t in l.smallSets, P t :=
  h₂.smallSets.frequently_iff.mpr fun _ hi => ⟨_, Subset.rfl, h₁ _ hi⟩

Frequent Property in Small Sets Filter via Basis

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$. If for every index $i$ with $p_i$ true, the property $P$ holds for $s_i$, then $P$ holds frequently in the filter $l.\text{smallSets}$ of small sets with respect to $l$. In other words, if $P(s_i)$ holds for all basis sets $s_i$ (with $p_i$ true), then there exists a frequently occurring collection of sets $t$ in $l.\text{smallSets}$ such that $P(t)$ holds.

Filter.Eventually.exists_mem_of_smallSets theorem

{p : Set α → Prop} (h : ∀ᶠ t in l.smallSets, p t) : ∃ s ∈ l, p s

Full source

theorem Eventually.exists_mem_of_smallSets {p : Set α → Prop}
    (h : ∀ᶠ t in l.smallSets, p t) : ∃ s ∈ l, p s :=
  h.exists_mem_basis_of_smallSets l.basis_sets

Existence of a Set in Filter Satisfying Eventual Property in Small Sets Filter

Informal description

For any predicate $p$ on subsets of $\alpha$, if $p(t)$ holds eventually for all sets $t$ in the small sets filter $l.\text{smallSets}$, then there exists a set $s \in l$ such that $p(s)$ holds.

Filter.tendsto_smallSets_iff theorem

{f : α → Set β} : Tendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ x in la, f x ⊆ t

Full source

/-- `g` converges to `f.smallSets` if for all `s ∈ f`, eventually we have `g x ⊆ s`. -/
theorem tendsto_smallSets_iff {f : α → Set β} :
    TendstoTendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ x in la, f x ⊆ t :=
  (hasBasis_smallSets lb).tendsto_right_iff

Characterization of Convergence to Small Sets Filter: $f \to l_b.\text{smallSets}$ iff $f(x) \subseteq t$ eventually for all $t \in l_b$

Informal description

A function $f : \alpha \to \text{Set } \beta$ tends to the small sets filter $l_b.\text{smallSets}$ along a filter $l_a$ if and only if for every set $t \in l_b$, the set $\{x \in \alpha \mid f(x) \subseteq t\}$ is eventually in $l_a$. In other words, $f$ converges to $l_b.\text{smallSets}$ if for every $t$ in the filter $l_b$, the values of $f$ are eventually subsets of $t$.

Filter.eventually_smallSets theorem

{p : Set α → Prop} : (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t, t ⊆ s → p t

Full source

theorem eventually_smallSets {p : Set α → Prop} :
    (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t, t ⊆ s → p t :=
  eventually_lift'_iff monotone_powerset

Characterization of Eventually Small Sets in a Filter

Informal description

For any predicate $p$ on subsets of $\alpha$, the statement "eventually for all small sets $s$ in the filter $l.\text{smallSets}$, $p(s)$ holds" is equivalent to the existence of a set $s \in l$ such that for all subsets $t \subseteq s$, $p(t)$ holds.

Filter.eventually_smallSets' theorem

 {p : Set α → Prop} (hp : ∀ ⦃s t⦄, s ⊆ t → p t → p s) : (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, p s

Full source

theorem eventually_smallSets' {p : Set α → Prop} (hp : ∀ ⦃s t⦄, s ⊆ t → p t → p s) :
    (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, p s :=
  eventually_smallSets.trans <|
    exists_congr fun s => Iff.rfl.and ⟨fun H => H s Subset.rfl, fun hs _t ht => hp ht hs⟩

Antitone Predicate Characterization for Eventually Small Sets in a Filter

Informal description

For any predicate $p$ on subsets of $\alpha$ that is antitone (i.e., if $s \subseteq t$ and $p(t)$ holds, then $p(s)$ holds), the statement "eventually for all small sets $s$ in the filter $l.\text{smallSets}$, $p(s)$ holds" is equivalent to the existence of a set $s \in l$ such that $p(s)$ holds.

Filter.frequently_smallSets theorem

{p : Set α → Prop} : (∃ᶠ s in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s, s ⊆ t ∧ p s

Full source

theorem frequently_smallSets {p : Set α → Prop} :
    (∃ᶠ s in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s, s ⊆ t ∧ p s :=
  l.hasBasis_smallSets.frequently_iff

Frequent Property Criterion for Small Sets Filter: $\exists^f s \in l.\text{smallSets}, p(s) \leftrightarrow \forall t \in l, \exists s \subseteq t, p(s)$

Informal description

For any predicate $p$ on subsets of $\alpha$, the following are equivalent: 1. The predicate $p$ holds frequently in the filter $l.\text{smallSets}$ (i.e., $\exists^f s \in l.\text{smallSets}, p(s)$). 2. For every set $t \in l$, there exists a subset $s \subseteq t$ such that $p(s)$ holds.

Filter.frequently_smallSets_mem theorem

(l : Filter α) : ∃ᶠ s in l.smallSets, s ∈ l

Full source

theorem frequently_smallSets_mem (l : Filter α) : ∃ᶠ s in l.smallSets, s ∈ l :=
  frequently_smallSets.2 fun t ht => ⟨t, Subset.rfl, ht⟩

Frequent Membership in Small Sets Filter: $\exists^f s \in l.\text{smallSets}, s \in l$

Informal description

For any filter $l$ on a type $\alpha$, the property that a set $s$ belongs to $l$ holds frequently in the filter $l.\text{mallSets}$, i.e., $\exists^f s \in l.\text{smallSets}, s \in l$.

Filter.tendsto_image_smallSets theorem

{f : α → β} : Tendsto (f '' ·) la.smallSets lb.smallSets ↔ Tendsto f la lb

Full source

@[simp]
lemma tendsto_image_smallSets {f : α → β} :
    TendstoTendsto (f '' ·) la.smallSets lb.smallSets ↔ Tendsto f la lb := by
  rw [tendsto_smallSets_iff]
  refine forall₂_congr fun u hu ↦ ?_
  rw [eventually_smallSets' fun s t hst ht ↦ (image_subset _ hst).trans ht]
  simp only [image_subset_iff, exists_mem_subset_iff, mem_map]

Image Convergence Criterion for Small Sets Filters: $f(S) \to l_b.\text{smallSets}$ iff $f \to l_b$

Informal description

For any function $f \colon \alpha \to \beta$, the following are equivalent: 1. The image map $S \mapsto f(S)$ tends to the small sets filter $l_b.\text{smallSets}$ along $l_a.\text{smallSets}$. 2. The function $f$ tends to the filter $l_b$ along $l_a$. In other words, $\lim_{S \to l_a.\text{smallSets}} f(S) = l_b.\text{smallSets}$ if and only if $\lim_{x \to l_a} f(x) = l_b$.

Filter.HasAntitoneBasis.tendsto_smallSets theorem

{ι} [Preorder ι] {s : ι → Set α} (hl : l.HasAntitoneBasis s) : Tendsto s atTop l.smallSets

Full source

theorem HasAntitoneBasis.tendsto_smallSets {ι} [Preorder ι] {s : ι → Set α}
    (hl : l.HasAntitoneBasis s) : Tendsto s atTop l.smallSets :=
  tendsto_smallSets_iff.2 fun _t ht => hl.eventually_subset ht

Convergence of Antitone Basis to Small Sets Filter: $s \to l.\text{smallSets}$ along $\text{atTop}$

Informal description

Let $\iota$ be a preorder and $\alpha$ a type. Given a filter $l$ on $\alpha$ with an antitone basis $s : \iota \to \text{Set } \alpha$, the function $s$ tends to the small sets filter $l.\text{smallSets}$ along the `atTop` filter on $\iota$. In other words, for every set $t \in l$, there exists an index $i_0 \in \iota$ such that for all $i \geq i_0$ in $\iota$, the set $s(i)$ is a subset of $t$.

Filter.monotone_smallSets theorem

: Monotone (@smallSets α)

Full source

@[mono]
theorem monotone_smallSets : Monotone (@smallSets α) :=
  monotone_lift' monotone_id monotone_const

Monotonicity of the Small Sets Filter Operation

Informal description

The operation `smallSets` that maps a filter `l` to the filter of small sets with respect to `l` is a monotone function. That is, for any two filters `l₁` and `l₂` on a type `α`, if `l₁ ≤ l₂` in the order of filters (i.e., `l₂` is finer than `l₁`), then `l₁.smallSets ≤ l₂.smallSets`.

Filter.smallSets_bot theorem

: (⊥ : Filter α).smallSets = pure ∅

Full source

@[simp]
theorem smallSets_bot : (⊥ : Filter α).smallSets = pure ∅ := by
  rw [smallSets, lift'_bot, powerset_empty, principal_singleton]
  exact monotone_powerset

Small Sets Filter of Bottom Filter Equals Singleton Empty Set

Informal description

The filter of small sets with respect to the bottom filter on a type $\alpha$ is equal to the pure filter containing only the empty set, i.e., $(\bot : \text{Filter } \alpha).\text{smallSets} = \{\emptyset\}$.

Filter.smallSets_top theorem

: (⊤ : Filter α).smallSets = ⊤

Full source

@[simp]
theorem smallSets_top : (⊤ : Filter α).smallSets = ⊤ := by
  rw [smallSets, lift'_top, powerset_univ, principal_univ]

Small Sets Filter of Top Filter Equals Top Filter

Informal description

The filter of small sets with respect to the top filter on a type $\alpha$ is equal to the top filter on the type of sets over $\alpha$, i.e., $(\top : \text{Filter } \alpha).\text{smallSets} = \top$.

Filter.smallSets_principal theorem

(s : Set α) : (𝓟 s).smallSets = 𝓟 (𝒫 s)

Full source

@[simp]
theorem smallSets_principal (s : Set α) : (𝓟 s).smallSets = 𝓟 (𝒫 s) :=
  lift'_principal monotone_powerset

Small Sets Filter of Principal Filter Equals Principal Filter of Powerset

Informal description

For any set $s$ in a type $\alpha$, the filter of small sets with respect to the principal filter generated by $s$ is equal to the principal filter generated by the powerset of $s$, i.e., $(\mathfrak{P} s).\text{smallSets} = \mathfrak{P}(\mathcal{P}(s))$.

Filter.smallSets_comap_eq_comap_image theorem

(l : Filter β) (f : α → β) : (comap f l).smallSets = comap (image f) l.smallSets

Full source

theorem smallSets_comap_eq_comap_image (l : Filter β) (f : α → β) :
    (comap f l).smallSets = comap (image f) l.smallSets := by
  refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_
  simp [Function.comp_def, map_bind, bind_map]

Equality of Small Sets Filter for Preimage and Image Preimage

Informal description

For any filter $l$ on a type $\beta$ and any function $f : \alpha \to \beta$, the filter of small sets with respect to the preimage filter $\text{comap}_f l$ is equal to the preimage filter of $l.\text{smallSets}$ under the image map $\text{image}_f : \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$. In other words: $$(\text{comap}_f l).\text{smallSets} = \text{comap}_{\text{image}_f} (l.\text{smallSets})$$

Filter.smallSets_comap theorem

(l : Filter β) (f : α → β) : (comap f l).smallSets = l.lift' (powerset ∘ preimage f)

Full source

theorem smallSets_comap (l : Filter β) (f : α → β) :
    (comap f l).smallSets = l.lift' (powersetpowerset ∘ preimage f) :=
  comap_lift'_eq2 monotone_powerset

Small Sets Filter of Preimage Equals Lifted Powerset-Preimage Composition

Informal description

For any filter $l$ on a type $\beta$ and any function $f : \alpha \to \beta$, the filter of small sets with respect to the preimage filter $\text{comap}_f l$ is equal to the filter obtained by lifting the composition of the powerset operation with the preimage of $f$ over $l$. More precisely, we have: $$(\text{comap}_f l).\text{smallSets} = l.\text{lift}' (\mathcal{P} \circ f^{-1})$$ where: - $\text{comap}_f l$ is the preimage filter of $l$ under $f$, - $\mathcal{P}$ denotes the powerset operation, and - $f^{-1}$ denotes the preimage under $f$.

Filter.comap_smallSets theorem

(l : Filter β) (f : α → Set β) : comap f l.smallSets = l.lift' (preimage f ∘ powerset)

Full source

theorem comap_smallSets (l : Filter β) (f : α → Set β) :
    comap f l.smallSets = l.lift' (preimagepreimage f ∘ powerset) :=
  comap_lift'_eq

Preimage of Small Sets Filter Equals Lifted Powerset-Preimage Composition

Informal description

For any filter $l$ on a type $\beta$ and any function $f : \alpha \to \mathcal{P}(\beta)$, the preimage filter of $l.\text{smallSets}$ under $f$ is equal to the filter generated by lifting the composition of the preimage of $f$ with the powerset operation over $l$. More precisely, we have: \[ \text{comap}_f (l.\text{smallSets}) = l.\text{lift}' (\mathcal{P} \circ f^{-1}) \] where: - $\text{comap}_f$ denotes the preimage filter construction, - $l.\text{smallSets}$ is the filter of small sets with respect to $l$, - $\mathcal{P}$ is the powerset operation, and - $f^{-1}$ is the preimage of $f$.

Filter.smallSets_iInf theorem

{f : ι → Filter α} : (iInf f).smallSets = ⨅ i, (f i).smallSets

Full source

theorem smallSets_iInf {f : ι → Filter α} : (iInf f).smallSets = ⨅ i, (f i).smallSets :=
  lift'_iInf_of_map_univ (powerset_inter _ _) powerset_univ

Infimum of Small Sets Filters Equals Small Sets Filter of Infimum

Informal description

For any family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$, the filter of small sets with respect to the infimum filter $\bigsqcap_i f_i$ is equal to the infimum of the filters of small sets with respect to each $f_i$. That is, $$(\bigsqcap_i f_i).\text{smallSets} = \bigsqcap_i (f_i.\text{smallSets}).$$

Filter.smallSets_inf theorem

(l₁ l₂ : Filter α) : (l₁ ⊓ l₂).smallSets = l₁.smallSets ⊓ l₂.smallSets

Full source

theorem smallSets_inf (l₁ l₂ : Filter α) : (l₁ ⊓ l₂).smallSets = l₁.smallSets ⊓ l₂.smallSets :=
  lift'_inf _ _ powerset_inter

Small Sets Filter Preserves Infima

Informal description

For any two filters $l_1$ and $l_2$ on a type $\alpha$, the filter of small sets with respect to their infimum equals the infimum of their respective small sets filters. That is, $$(l_1 \sqcap l_2).\text{smallSets} = l_1.\text{smallSets} \sqcap l_2.\text{smallSets}.$$

Filter.smallSets_neBot instance

(l : Filter α) : NeBot l.smallSets

Full source

instance smallSets_neBot (l : Filter α) : NeBot l.smallSets := by
  refine (lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty
  exact monotone_powerset

Nonemptiness of the Small Sets Filter

Informal description

For any filter $l$ on a type $\alpha$, the filter of small sets $l.\text{smallSets}$ is nonempty.

Filter.Tendsto.smallSets_mono theorem

{s t : α → Set β} (ht : Tendsto t la lb.smallSets) (hst : ∀ᶠ x in la, s x ⊆ t x) : Tendsto s la lb.smallSets

Full source

theorem Tendsto.smallSets_mono {s t : α → Set β} (ht : Tendsto t la lb.smallSets)
    (hst : ∀ᶠ x in la, s x ⊆ t x) : Tendsto s la lb.smallSets := by
  rw [tendsto_smallSets_iff] at ht ⊢
  exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)

Monotonicity of Convergence to Small Sets Filter: $s \subseteq t$ implies $s \to l_b.\text{smallSets}$ if $t \to l_b.\text{smallSets}$

Informal description

Let $s, t : \alpha \to \text{Set } \beta$ be functions mapping to sets. If $t$ tends to the small sets filter $l_b.\text{smallSets}$ along the filter $l_a$, and if for eventually all $x$ in $l_a$ we have $s(x) \subseteq t(x)$, then $s$ also tends to $l_b.\text{smallSets}$ along $l_a$. In other words, if $t$ converges to the small sets filter and $s$ is eventually pointwise smaller than $t$, then $s$ also converges to the small sets filter.

Filter.Tendsto.of_smallSets theorem

 {s : α → Set β} {f : α → β} (hs : Tendsto s la lb.smallSets) (hf : ∀ᶠ x in la, f x ∈ s x) : Tendsto f la lb

Full source

/-- 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'`. -/
theorem Tendsto.of_smallSets {s : α → Set β} {f : α → β} (hs : Tendsto s la lb.smallSets)
    (hf : ∀ᶠ x in la, f x ∈ s x) : Tendsto f la lb := fun t ht =>
  hf.mp <| (tendsto_smallSets_iff.mp hs t ht).mono fun _ h₁ h₂ => h₁ h₂

Generalized Squeeze Theorem for Filters

Informal description

Let $s : \alpha \to \text{Set } \beta$ be a family of sets and $f : \alpha \to \beta$ be a function. If $s$ tends to the small sets filter $l_b.\text{smallSets}$ along a filter $l_a$, and $f(x) \in s(x)$ holds eventually along $l_a$, then $f$ tends to $l_b$ along $l_a$.

Filter.eventually_smallSets_eventually theorem

{p : α → Prop} : (∀ᶠ s in l.smallSets, ∀ᶠ x in l', x ∈ s → p x) ↔ ∀ᶠ x in l ⊓ l', p x

Full source

@[simp]
theorem eventually_smallSets_eventually {p : α → Prop} :
    (∀ᶠ s in l.smallSets, ∀ᶠ x in l', x ∈ s → p x) ↔ ∀ᶠ x in l ⊓ l', p x :=
  calc
    _ ↔ ∃ s ∈ l, ∀ᶠ x in l', x ∈ s → p x :=
      eventually_smallSets' fun _ _ hst ht => ht.mono fun _ hx hs => hx (hst hs)
    _ ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x, x ∈ t → x ∈ s → p xcalc
    _ ↔ ∃ s ∈ l, ∀ᶠ x in l', x ∈ s → p x :=
      eventually_smallSets' fun _ _ hst ht => ht.mono fun _ hx hs => hx (hst hs)
    _ ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x, x ∈ t → x ∈ s → p x := by simp only [eventually_iff_exists_mem]
    _ ↔ ∀ᶠ x in l ⊓ l', p x := by simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]

Equivalence of Eventual Small Sets and Filter Intersection for Predicate Satisfaction

Informal description

For any predicate $p$ on elements of type $\alpha$, the following are equivalent: 1. For eventually all small sets $s$ in the filter $l.\text{smallSets}$, and for eventually all $x$ in the filter $l'$, if $x \in s$ then $p(x)$ holds. 2. For eventually all $x$ in the filter $l \sqcap l'$, $p(x)$ holds.

Filter.eventually_smallSets_forall theorem

{p : α → Prop} : (∀ᶠ s in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ x in l, p x

Full source

@[simp]
theorem eventually_smallSets_forall {p : α → Prop} :
    (∀ᶠ s in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ x in l, p x := by
  simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p

Equivalence of Small Sets Universality and Filter Eventuality

Informal description

For any predicate $p$ on elements of type $\alpha$, the following are equivalent: 1. For eventually all sets $s$ in the filter $l.\text{smallSets}$, the predicate $p(x)$ holds for all $x \in s$. 2. For eventually all $x$ in the filter $l$, the predicate $p(x)$ holds.

Filter.eventually_smallSets_subset theorem

{s : Set α} : (∀ᶠ t in l.smallSets, t ⊆ s) ↔ s ∈ l

Full source

@[simp]
theorem eventually_smallSets_subset {s : Set α} : (∀ᶠ t in l.smallSets, t ⊆ s) ↔ s ∈ l :=
  eventually_smallSets_forall

Equivalence of Eventual Small Sets Subset and Filter Membership

Informal description

For any set $s$ in a type $\alpha$, the following are equivalent: 1. For eventually all sets $t$ in the filter $l.\text{smallSets}$, $t$ is a subset of $s$. 2. The set $s$ belongs to the filter $l$.