Mathlib.Algebra.Order.PartialSups

 [Add ι] [One ι] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccAddOrder ι] (f : ι → α) (i : ι) :
  partialSups f (i + 1) = partialSups f i ⊔ f (i + 1)

Full source

@[simp]
lemma partialSups_add_one [Add ι] [One ι] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccAddOrder ι]
    (f : ι → α) (i : ι) : partialSups f (i + 1) = partialSupspartialSups f i ⊔ f (i + 1) :=
  Order.succ_eq_add_one i ▸ partialSups_succ f i

Recursive Formula for Partial Suprema in a Successor-Additive Order

Informal description

Let $\iota$ be a linearly ordered type with a locally finite order structure where all intervals bounded below are finite, and equipped with a successor function satisfying the `SuccAddOrder` condition. For any function $f : \iota \to \alpha$ and any element $i \in \iota$, the partial supremum of $f$ at $i + 1$ is equal to the supremum of the partial supremum of $f$ at $i$ and the value $f(i + 1)$. In other words, \[ \text{partialSups}\, f\, (i + 1) = \text{partialSups}\, f\, i \sqcup f(i + 1). \]