chore: fix align statement (#1853)

leanprover-community · Jan 26, 2023 · b5d2e9a · b5d2e9a
1 parent e32b06c
commit b5d2e9a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean
@@ -1513,7 +1513,7 @@ noncomputable nonrec def Ultrafilter.lim (F : Ultrafilter α) : α :=
 at `f`, if it exists. -/
 noncomputable def limUnder [Nonempty α] (f : Filter β) (g : β → α) : α :=
   lim (f.map g)
-#align lim lim
+#align lim limUnder
 
 /-- If a filter `f` is majorated by some `𝓝 a`, then it is majorated by `𝓝 (Filter.lim f)`. We
 formulate this lemma with a `[Nonempty α]` argument of `lim` derived from `h` to make it useful for