DominatedFinMeasAdditive — Mathlib

English

If μ s = 0 for a measurable set s, then T(s) = 0 for dominated FinMeasAdditive T.

Русский

Если μ(s)=0 для измеримого s, то T(s)=0 для доминированной FinMeasAdditive.

LaTeX

$$μ s = 0 → T s = 0$$

Lean4

/-- A `FinMeasAdditive` set function whose norm on every set is less than the measure of the
set (up to a multiplicative constant). -/
def DominatedFinMeasAdditive {β} [SeminormedAddCommGroup β] {_ : MeasurableSpace α} (μ : Measure α) (T : Set α → β)
    (C : ℝ) : Prop :=
  FinMeasAdditive μ T ∧ ∀ s, MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s

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