piecewise_mul — Mathlib

English

Piecewise product distributes: the piecewise of (f1 f2) and (g1 g2) equals the product of piecewise f1,g1 and piecewise f2,g2.

Русский

Разбиение на куски умножения распределяется: piecewise (f1 f2) (g1 g2) = piecewise f1 g1 · piecewise f2 g2.

LaTeX

$$$s.piecewise (f_1 \cdot f_2) (g_1 \cdot g_2) = s.piecewise f_1 g_1 \cdot s.piecewise f_2 g_2$$$

Lean4

@[to_additive]
theorem piecewise_mul [∀ i, Mul (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)] (f₁ f₂ g₁ g₂ : ∀ i, f i) :
    s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂ :=
  s.piecewise_op₂ f₁ _ _ _ fun _ => (· * ·)

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