fix: align statement for infi is currently wrong (#1187)

leanprover-community · Dec 23, 2022 · 101a430 · 101a430
1 parent d90ae09
commit 101a430
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Order/CompleteLattice.lean b/Mathlib/Order/CompleteLattice.lean
@@ -86,7 +86,7 @@ def supᵢ [SupSet α] {ι} (s : ι → α) : α :=
 /-- Indexed infimum -/
 def infᵢ [InfSet α] {ι} (s : ι → α) : α :=
   infₛ (range s)
-#align infᵢ infᵢ
+#align infi infᵢ
 
 instance (priority := 50) infSet_to_nonempty (α) [InfSet α] : Nonempty α :=
   ⟨infₛ ∅⟩