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