doc: fix docstring of liminf_const_add (#22280)

Thanks to Vasudev Joy on the Xena Discord for spotting this.
leanprover-community · Feb 25, 2025 · 10601ef · 10601ef
1 parent 6d33eaf
commit 10601ef
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
@@ -543,7 +543,7 @@ lemma limsup_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
   (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x + c)
     (fun _ _ h ↦ add_le_add_right h c) (continuous_add_right c).continuousAt bdd_above cobdd).symm
 
-/-- `liminf (c + xᵢ) = c + limsup xᵢ`. -/
+/-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
 lemma liminf_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
     [AddLeftMono R] (f : ι → R) (c : R)
     (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :