Results about partialSups of functions taking values in a Group

theorem partialSups_const_mul {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Group α] [Preorder ι] [LocallyFiniteOrderBot ι] [MulLeftMono α] (f : ι → α) (c : α) (i : ι) : (partialSups fun (x : ι) => c * f x) i = c * (partialSups f) i

theorem partialSups_const_add {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [AddGroup α] [Preorder ι] [LocallyFiniteOrderBot ι] [AddLeftMono α] (f : ι → α) (c : α) (i : ι) : (partialSups fun (x : ι) => c + f x) i = c + (partialSups f) i

theorem partialSups_mul_const {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Group α] [Preorder ι] [LocallyFiniteOrderBot ι] [MulRightMono α] (f : ι → α) (c : α) (i : ι) : (partialSups fun (x : ι) => f x * c) i = (partialSups f) i * c

theorem partialSups_add_const {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [AddGroup α] [Preorder ι] [LocallyFiniteOrderBot ι] [AddRightMono α] (f : ι → α) (c : α) (i : ι) : (partialSups fun (x : ι) => f x + c) i = (partialSups f) i + c