finite_of_finite_mconv — Mathlib

English

If μ and ν are finite measures, then μ ∗ₘ ν is finite.

Русский

Если μ и ν конечны, то μ ∗ₘ ν также конечна.

LaTeX

$$$ \text{If } \mu, \nu \text{ are finite, then } (\mu ∗ₘ ν) \text{ is finite.}$$$

Lean4

@[to_additive]
instance finite_of_finite_mconv (μ : Measure M) (ν : Measure M) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    IsFiniteMeasure (μ ∗ₘ ν) :=
  by
  have h : (μ ∗ₘ ν) Set.univ < ⊤ := by
    unfold mconv
    exact IsFiniteMeasure.measure_univ_lt_top
  exact { measure_univ_lt_top := h }

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