piecewise_smul — Mathlib

English

If a set s⊆ι and a scalar c act on a family f₁,g₁: ∀i, α_i, then s.piecewise (c•f₁) (c•g₁) = c• s.piecewise f₁ g₁.

Русский

Пусть s⊆ι и скаляры действуют по координатам. Тогда функция piecewise от {c•f₁} и {c•g₁} равна c• piecewise f₁ g₁.

LaTeX

$$$s.{\text{piecewise}}\left(c\cdot f_1,\; c\cdot g_1\right)= c\cdot s.{\text{piecewise}}(f_1,g_1).$$$

Lean4

@[to_additive]
theorem piecewise_smul [∀ i, SMul M (α i)] (s : Set ι) [∀ i, Decidable (i ∈ s)] (c : M) (f₁ g₁ : ∀ i, α i) :
    s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁ :=
  s.piecewise_op (δ' := α) f₁ _ fun _ ↦ (c • ·)

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