mk_mul_mk — Mathlib

English

There is a Monoid structure on the space of almost everywhere equal functions α →ₘ[μ] γ, with identity given by the constant zero/germ and multiplication defined pointwise.

Русский

У пространства почти всюду равных функций α →ₘ[μ] γ существует структура моноида: тождественный элемент — константная ноль/герм, унарный функтор — точечное произведение.

LaTeX

$$$\text{Monoid}(α \to_{μ} γ)$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_mul_mk (f g : α → γ) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
    (mk f hf : α →ₘ[μ] γ) * mk g hg = mk (f * g) (hf.mul hg) :=
  rfl

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