setToL1SCLM_congr_left — Mathlib

English

If two dominating families T and T' are equal as functions on all measurable sets, then they induce the same L1-transfer on simple functions.

Русский

Если две доминирующие семейства T и T' совпадают на всех измеримых множествах, то порождают одинаковое преобразование L1 на простых функциях.

LaTeX

$$$setToL1SCLM\;\alpha\;E\;\mu\;hT\;f = setToL1SCLM\;\alpha\;E\;\mu\;hT'\;f$$$

Lean4

theorem setToL1SCLM_congr_left (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
    (h : T = T') (f : α →₁ₛ[μ] E) : setToL1SCLM α E μ hT f = setToL1SCLM α E μ hT' f :=
  setToL1S_congr_left T T' (fun _ _ _ => by rw [h]) f

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