doc(order/filter/small_sets): fix in doc (#13648)

leanprover-community · Apr 28, 2022 · 220d4b8 · 220d4b8
1 parent c096a33
commit 220d4b8
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/order/filter/small_sets.lean b/src/order/filter/small_sets.lean
@@ -13,9 +13,9 @@ 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.
+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