<commit_before>/-
Copyright (c) 2022 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>
-/
import order.filter.lift

/-!
# 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.small_sets` if for all `s ∈ f`, eventually we have `g x ⊆ s`.

An example usage is that if `f : ι → ℝ` is a family of nonnegative functions with integral 1, then
saying that `f` tendsto `(𝓝 0).small_sets` is a way of saying that `f` tends to the Dirac delta
distribution.
-/

open_locale filter
open filter set

variables {α β : Type*} {ι : Sort*}

namespace filter

variables {l l' la : filter α} {lb : filter β}

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

lemma small_sets_eq_generate {f : filter α} : f.small_sets = generate (powerset '' f.sets) :=
by { simp_rw [generate_eq_binfi, small_sets, infi_image], refl }

lemma has_basis.small_sets {p : ι → Prop} {s : ι → set α}
  (h : has_basis l p s) : has_basis l.small_sets p (λ i, 𝒫 (s i)) :=
h.lift' monotone_powerset
<commit_msg>doc(order/filter/small_sets): fix in doc (#13648)<commit_after>/-
Copyright (c) 2022 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>
-/
import order.filter.lift

/-!
# 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.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.
-/

open_locale filter
open filter set

variables {α β : Type*} {ι : Sort*}

namespace filter

variables {l l' la : filter α} {lb : filter β}

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

lemma small_sets_eq_generate {f : filter α} : f.small_sets = generate (powerset '' f.sets) :=
by { simp_rw [generate_eq_binfi, small_sets, infi_image], refl }

lemma has_basis.small_sets {p : ι → Prop} {s : ι → set α}
  (h : has_basis l p s) : has_basis l.small_sets p (λ i, 𝒫 (s i)) :=
h.lift' monotone_powerset

{'fraction_non_alphanumeric': 0.11666666666666667, 'fraction_numerical': 0.007954545454545454, 'mean_word_length': 3.75, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7567432', 'n_tokens_mistral': 979, 'n_tokens_neox': 916, 'n_words': 404}