Theorems · Theorem · order theory

partialSups_add_const

∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : AddGroup α] [inst_2 : Preorder ι]
  [inst_3 : LocallyFiniteOrderBot ι] [AddRightMono α] (f : ι → α) (c : α) (i : ι),
  (partialSups fun x => f x + c) i = (partialSups f) i + c

Defined in

Mathlib.Algebra.Order.Group.PartialSups

Cited by

0 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemilatticeSupAddGroupPreorderLocallyFiniteOrderBotAddRightMono