mul — Mathlib

English

If f and g have finite μ-measurable support and β is a MulZeroClass, then the product f*g has finite μ-measurable support.

Русский

Если f и g имеют конечную μ-опору и β — MulZeroClass, тогда произведение f*g имеет конечную μ-опору.

LaTeX

$$$\mathrm{FinMeasSupp}(f,\mu) \land \mathrm{FinMeasSupp}(g,\mu) \Rightarrow \mathrm{FinMeasSupp}(f \cdot g,\mu)$$$

Lean4

protected theorem mul {β} [MulZeroClass β] {f g : α →ₛ β} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) :
    (f * g).FinMeasSupp μ := by
  rw [mul_eq_map₂]
  exact hf.map₂ hg (zero_mul 0)

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