doc(topology/uniform_space/cauchy): fix typo (#12453)

leanprover-community · Mar 5, 2022 · 2840532 · 2840532
1 parent bda091d
commit 2840532
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean
@@ -470,7 +470,7 @@ let ⟨t', ht', hct', htt'⟩ := mem_uniformity_is_closed ht, ⟨c, hcf, hc⟩ :
     ... ⊆ _ : Union₂_subset $ assume i hi, subset.trans (assume x, @htt' (x, i))
       (subset_bUnion_of_mem hi)⟩
 
-/-- The image of a totally bounded set under a unifromly continuous map is totally bounded. -/
+/-- The image of a totally bounded set under a uniformly continuous map is totally bounded. -/
 lemma totally_bounded.image [uniform_space β] {f : α → β} {s : set α}
   (hs : totally_bounded s) (hf : uniform_continuous f) : totally_bounded (f '' s) :=
 assume t ht,