piecewise_div — Mathlib

English

Piecewise division distributes: s.piecewise (f1 / f2) (g1 / g2) = s.piecewise f1 g1 / s.piecewise f2 g2.

Русский

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

LaTeX

$$$s.piecewise (f_1 / f_2) (g_1 / g_2) = s.piecewise f_1 g_1 / s.piecewise f_2 g_2$$$

Lean4

@[to_additive]
theorem piecewise_div [∀ i, Div (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 _ => (· / ·)

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