partialSups_add_one — Mathlib

English

For a function f : ι → α into a semilattice, the value at i+1 equals the join of the previous value with f(i+1): partialSups f (i+1) = partialSups f i ⊔ f(i+1).

Русский

Для функции f: ι → α, значения в i+1 равно объединению предыдущего значения и f(i+1): partialSups f (i+1) = partialSups f i ⊔ f(i+1).

LaTeX

$$$\forall f:\, ι \to α\,\bigl( partialSups\ f\ (i+1) = partialSups\ f\ i \;\sqcup\; f\ (i+1) \bigr)$$$

Lean4

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

Похожие утверждения