English
In a linear order with successor, the value at succ i is the join of the value at i with f(succ i): partialSups f(succ i) = partialSups f(i) ⊔ f(succ i).
Русский
В линейном порядке с переходом к следующему элементу, значение на succ i равняется объединению предыдущего значения и f(succ i).
LaTeX
$$$\\partialSups f(\\mathrm{succ}\\, i) = \\partialSups f(i) \\;\\sqcup\\; f(\\mathrm{succ}\\, i)$$$
Lean4
@[simp]
theorem partialSups_succ [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] (f : ι → α) (i : ι) :
partialSups f (Order.succ i) = partialSups f i ⊔ f (Order.succ i) :=
by
suffices Iic (Order.succ i) = Iic i ∪ {Order.succ i} by
simp only [partialSups_apply, this, sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]
ext
simp only [mem_Iic, mem_union, mem_singleton]
constructor
· exact fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm
· exact fun h ↦ h.elim (le_trans · <| Order.le_succ _) le_of_eq
