English
If f : ι → α and i ∈ ι, then partialSups f (i + 1) = f(⊥) ⊔ partialSups (f ∘ (k ↦ k + 1)) i, given an additive structure on ι and suitable order properties.
Русский
Если f : ι → α и i ∈ ι, то partialSups f (i + 1) = f(⊥) ⊔ partialSups (f ∘ (k ↦ k + 1)) i, при наличии аддитивной структуры на ι и подходящих свойств порядка.
LaTeX
$$partialSups f (i + 1) = f(⊥) ⊔ partialSups (f ∘ (fun k ↦ k + 1)) i$$
Lean4
/-- See `partialSups_add_one` for another decomposition of `partialSups f (i + 1)`. -/
theorem partialSups_add_one' [Add ι] [One ι] [OrderBot ι] [LocallyFiniteOrder ι] [SuccAddOrder ι] (f : ι → α) (i : ι) :
partialSups f (i + 1) = f ⊥ ⊔ partialSups (f ∘ (fun k ↦ k + 1)) i := by
simpa [← Order.succ_eq_add_one] using partialSups_succ' f i
