norm_setToL1SCLM_le — Mathlib

English

The operator norm of setToL1SCLM is bounded above by C whenever hT is dominated with constant C ≥ 0.

Русский

Нормированное операторное отображение setToL1SCLM не превосходит константу C при условии, что hT доминирует с константой C ≥ 0.

LaTeX

$$$\|setToL1SCLM\;α\;E\;μ\;hT\| ≤ C$$$

Lean4

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

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