feat(Order/Filter/Extr): local minimum and local maximum implies const (#34032)

Author: b-mehta

Mathlib/Order/Filter/Extr.lean

@@ -195,6 +195,12 @@ theorem isMaxOn_const {b : β} : IsMaxOn (fun _ => b) s a :=
 theorem isExtrOn_const {b : β} : IsExtrOn (fun _ => b) s a :=
   isExtrFilter_const
 
+/-- If `f` has a minimum and a maximum both given by `f a` along the filter `l`, then it is
+eventually equal to `f a` along the filter. -/
+lemma eventuallyEq_of_isMinFilter_of_isMaxFilter {β : Type*} [PartialOrder β] {f : α → β}
+    (h₁ : IsMinFilter f l a) (h₂ : IsMaxFilter f l a) : f =ᶠ[l] (fun _ ↦ f a) := by
+  filter_upwards [h₁, h₂] using by grind
+
 /-! ### Order dual -/