setToFun_congr_left — Mathlib

English

If T and T' agree on all measurable finite-measure s, then setToFun μ T hT f = setToFun μ T' hT' f for all f.

Русский

Если T и T' совпадают на всем измеримом конечном по мере s, то setToFun μ T hT f = setToFun μ T' hT' f для всех f.

LaTeX

$$$\forall s, \text{MeasurableSet}(s) \Rightarrow T s = T' s \Rightarrow setToFun\, μ\, T\, h_T\, f = setToFun\, μ\, T'\, h_T'\, f$$$

Lean4

theorem setToFun_congr_left (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T')
    (f : α → E) : setToFun μ T hT f = setToFun μ T' hT' f :=
  by
  by_cases hf : Integrable f μ
  · simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left T T' hT hT' h]
  · simp_rw [setToFun_undef _ hf]

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