PartialSups in a SuccAddOrder

Basic results concerning PartialSups which follow with minimal assumptions beyond the fact that the PartialSup is defined over a SuccAddOrder.

@[simp]

theorem partialSups_add_one {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [LinearOrder ι] [Add ι] [One ι] [LocallyFiniteOrderBot ι] [SuccAddOrder ι] (f : ι → α) (i : ι) : (partialSups f) (i + 1) = (partialSups f) i ⊔ f (i + 1)

theorem partialSups_succ' {ι : Type u_2} [LinearOrder ι] {α : Type u_3} [SemilatticeSup α] [LocallyFiniteOrder ι] [SuccOrder ι] [OrderBot ι] (f : ι → α) (i : ι) : (partialSups f) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) i

See partialSups_succ for another decomposition of (partialSups f) (Order.succ i).

theorem partialSups_add_one' {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [LinearOrder ι] [Add ι] [One ι] [OrderBot ι] [LocallyFiniteOrder ι] [SuccAddOrder ι] (f : ι → α) (i : ι) : (partialSups f) (i + 1) = f ⊥ ⊔ (partialSups (f ∘ fun (k : ι) => k + 1)) i

See partialSups_add_one for another decomposition of partialSups f (i + 1).