right_of_add_measure — Mathlib

English

If a function is in MemLp with respect to μ+ν, then it is in MemLp with respect to ν.

Русский

Если функция принадлежит MemLp относительно μ+ν, то она принадлежит MemLp относительно ν.

LaTeX

$$right_of_add_measure {f} (h : MemLp f p (μ + ν)) : MemLp f p ν.$$

Lean4

theorem right_of_add_measure {f : α → ε} (h : MemLp f p (μ + ν)) : MemLp f p ν :=
  h.mono_measure <| Measure.le_add_left <| le_refl _

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