doc: typo (#20829)

leanprover-community · Jan 18, 2025 · af5ebc2 · af5ebc2
1 parent 6cb9a2a
commit af5ebc2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Order/Restriction.lean b/Mathlib/Order/Restriction.lean
@@ -59,7 +59,7 @@ variable [LocallyFiniteOrderBot α]
 
 open Finset
 
-/-- Restrict domain of a function `f` indexed by `α` to elements `≤ α`, seen as a finite set. -/
+/-- Restrict domain of a function `f` indexed by `α` to elements `≤ a`, seen as a finite set. -/
 def frestrictLe (a : α) := (Iic a).restrict (π := π)
 
 @[simp]