Fix Lean3 typo

avigad · Dec 4, 2023 · 5480c69 · 5480c69
1 parent eda3ee9
commit 5480c69
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C09_Topology/S01_Filters.lean b/MIL/C09_Topology/S01_Filters.lean
@@ -364,7 +364,7 @@ example (x₀ : ℝ) : HasBasis (𝓝 x₀) (fun ε : ℝ ↦ 0 < ε) fun ε ↦
 
 /- TEXT:
 There is also a nice basis for the filter ``atTop``. The lemma
-``Filter.has_basis.tendsto_iff`` allows
+``Filter.HasBasis.tendsto_iff`` allows
 us to reformulate a statement of the form ``Tendsto f F G``
 given bases for ``F`` and ``G``.
 Putting these pieces together gives us essentially the notion of convergence