setToFun_congr_measure_of_add_right

English

If hT_add holds for μ+μ' and hT holds for μ, then for any Integrable f with respect to μ+μ', setToFun(μ+μ') T hT_add f equals setToFun μ T hT f.

Русский

Если верны условия на сумму справа, то для интегрируемой f по μ+μ' значения setToFun совпадают.

LaTeX

$$$\\mathrm{setToFun}(μ+μ',T,hT_{\\text{add}} f)=\\mathrm{setToFun}(μ,T,hT) f$$$

Lean4

theorem setToFun_congr_measure_of_add_right {μ' : Measure α} (hT_add : DominatedFinMeasAdditive (μ + μ') T C')
    (hT : DominatedFinMeasAdditive μ T C) (f : α → E) (hf : Integrable f (μ + μ')) :
    setToFun (μ + μ') T hT_add f = setToFun μ T hT f :=
  by
  refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf
  rw [one_smul]
  nth_rw 1 [← add_zero μ]
  exact add_le_add le_rfl bot_le

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