left_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

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

Lean4

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

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