lpMeasSubgroupToLpTrim_sub — Mathlib

English

Subtracting in the domain corresponds to subtraction after applying the trim-to-Lp map.

Русский

Вычитание в области соответствует вычитанию после применения обрезки.

LaTeX

$$$lpMeasSubgroupToLpTrim\ F\ p\ μ hm (f - g) = lpMeasSubgroupToLpTrim\ F\ p\ μ hm f - lpMeasSubgroupToLpTrim\ F\ p\ μ hm g$$$

Lean4

theorem lpMeasSubgroupToLpTrim_sub (hm : m ≤ m0) (f g : lpMeasSubgroup F m p μ) :
    lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g :=
  by rw [sub_eq_add_neg, sub_eq_add_neg, lpMeasSubgroupToLpTrim_add, lpMeasSubgroupToLpTrim_neg]

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