partialSups_mul_const — Mathlib

English

For f:ι → α and c ∈ α with α a semilattice-ordered group and MulRightMono, the equality partialSups(f · × c) = partialSups(f) · c holds.

Русский

Для f:ι → α и фиксированного c выполняется частичное суммирование с правым умножением: partialSups(f · c) = partialSups(f) · c.

LaTeX

$$partialSups (f · c) i = partialSups f i * c$$

Lean4

@[to_additive]
theorem partialSups_mul_const [MulRightMono α] (f : ι → α) (c : α) (i : ι) :
    partialSups (f · * c) i = partialSups f i * c :=
  map_partialSups (OrderIso.mulRight _) ..

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