partialSups_const_mul — Mathlib

English

If f is a function into a semilattice-ordered group α and c ∈ α, then partialSups(c · f) = c · partialSups(f).

Русский

Если f:ι → α, где α — полулинейное упорядоченное множество, и c ∈ α, то partialSups(c · f) = c · partialSups(f).

LaTeX

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

Lean4

@[to_additive]
theorem partialSups_const_mul [MulLeftMono α] (f : ι → α) (c : α) (i : ι) :
    partialSups (c * f ·) i = c * partialSups f i :=
  map_partialSups (OrderIso.mulLeft _) ..

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