From 536a17fbe243af50342cad78d4154abb70eb20ec Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 25 Feb 2025 11:05:38 +0000 Subject: [PATCH] doc: fix docstring of liminf_const_add --- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean index 5be53f4ed4e3c..e505ecb753c1c 100644 --- 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) :