norm_setToL1SCLM_le' — Mathlib

English

If T and T' dominate with C, C' and T s = T' s for all measurable s with finite measure, then the L1-transfer maps coincide on all simple functions.

Русский

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

LaTeX

$$$\forall s, MeasurableSet\; s,\; μ s < \infty \Rightarrow T s = T' s \Rightarrow setToL1SCLM α E μ hT f = setToL1SCLM α E μ hT' f$$$

Lean4

theorem norm_setToL1SCLM_le' {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) :
    ‖setToL1SCLM α E μ hT‖ ≤ max C 0 :=
  LinearMap.mkContinuous_norm_le' _ _

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