setToL1SCLM_zero_left' — Mathlib

English

If hT is as above and T s = 0 for all sem\-measurable s with μ s < ∞, then every α →₁ₛ[μ] E maps to 0 under setToL1SCLM.

Русский

Пусть hT удовлетворяет условию, и для каждого измеримого множества s с μ s < ∞ выполняется T s = 0; тогда любой f ∈ α →₁ₛ[μ] E отображается в 0 через setToL1SCLM.

LaTeX

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

Lean4

theorem setToL1SCLM_zero_left' (hT : DominatedFinMeasAdditive μ T C) (h_zero : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0)
    (f : α →₁ₛ[μ] E) : setToL1SCLM α E μ hT f = 0 :=
  setToL1S_zero_left' h_zero f

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