setToFun_congr_measure_of_add_left

English

For a dominated FinMeasAdditive hT and a function f, the truncation to ∞·μ yields zero for the corresponding setToFun, i.e., the top measure annihilates setToFun.

Русский

При умножении меры на бесконечность ∞·μ функция setToFun становится нулевой.

LaTeX

$$$\\mathrm{setToFun}(∞·μ, T, hT, f)=0$$$

Lean4

theorem setToFun_congr_measure_of_add_left {μ' : 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 [← zero_add μ']
  exact add_le_add_right bot_le μ'

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