English
Let α be a semilattice with bottom, and ι a locally finite order with successor. For f : ι → α and i ∈ ι, (partialSups f)(Order.succ i) = f(⊥) ⊔ (partialSups (f ∘ Order.succ)) i.
Русский
Пусть α — полугруппа-суперслой с нулём, и ι — локально конечный упорядоченный множитель с функцией successor. Тогда для любой f : ι → α и i ∈ ι выполняется равенство (partialSups f)(Order.succ i) = f(⊥) ⊔ (partialSups (f ∘ Order.succ)) i.
LaTeX
$$$ (partialSups\, f) (Order.succ\, i) = f\, (\bot) \sqcup (partialSups\, (f \circ Order.succ))\, i $$$
Lean4
/-- See `partialSups_succ` for another decomposition of `(partialSups f) (Order.succ i)`. -/
theorem partialSups_succ' {α : Type*} [SemilatticeSup α] [LocallyFiniteOrder ι] [SuccOrder ι] [OrderBot ι] (f : ι → α)
(i : ι) : (partialSups f) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) i :=
by
refine Succ.rec (by simp) (fun j _ h ↦ ?_) (bot_le (a := i))
have :
(partialSups (f ∘ Order.succ)) (Order.succ j) =
((partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)) :=
by simp
simp [this, h, sup_assoc]
