feat(Order/PartialSups): add exists_partialSups_eq

Author: lua-vr

Mathlib/Order/PartialSups.lean

@@ -9,6 +9,7 @@ public import Mathlib.Data.Set.Finite.Lattice
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
 public import Mathlib.Order.Interval.Finset.Nat
 public import Mathlib.Order.SuccPred.Basic
+import Mathlib.Data.Finset.Max
 
 /-!
 # The monotone sequence of partial supremums of a sequence
@@ -286,3 +287,23 @@ lemma partialSups_eq_biUnion_range (s : ℕ → Set α) (n : ℕ) :
   simp [partialSups_eq_biSup, Nat.lt_succ_iff]
 
 end Set
+
+section LinearOrder
+/-!
+### Functions taking values on some `LinearOrder`.
+-/
+
+variable [Preorder ι] [LocallyFiniteOrderBot ι] [LinearOrder α]
+
+/-- In a linear order, there exists an index which is equal to the value of `partialSups`. -/
+theorem exists_partialSups_eq (f : ι → α) (i : ι) :
+    ∃ j ≤ i, partialSups f i = f j := by
+  obtain ⟨j, hj⟩ : ∃ j ∈ Finset.Iic i, ∀ k ∈ Finset.Iic i, f k ≤ f j :=
+    Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩
+  simp_all only [Finset.mem_Iic, partialSups, OrderHom.coe_mk]
+  use j, hj.1
+  apply le_antisymm
+  · exact Finset.sup'_le _ _ fun k hk => hj.2 k (Finset.mem_Iic.1 hk)
+  · exact Finset.le_sup' _ (Finset.mem_Iic.2 hj.1 )
+
+end LinearOrder