chore: fix typo in docstring (#7612)

leanprover-community · Oct 10, 2023 · 6dbefa3 · 6dbefa3
1 parent d34032a
commit 6dbefa3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -478,7 +478,7 @@ theorem eventually_uniformity_iterate_comp_subset {s : Set (α × α)} (hs : s
       (compRel_mono hU.1 hU.2).trans hts⟩
 #align eventually_uniformity_iterate_comp_subset eventually_uniformity_iterate_comp_subset
 
-/-- If `s ∈ 𝓤 α`, then for any natural `n`, for a subset `t` of a sufficiently small set in `𝓤 α`,
+/-- If `s ∈ 𝓤 α`, then for a subset `t` of a sufficiently small set in `𝓤 α`,
 we have `t ○ t ⊆ s`. -/
 theorem eventually_uniformity_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
     ∀ᶠ t in (𝓤 α).smallSets, t ○ t ⊆ s :=