zero — Mathlib

English

A FinMeasAdditive function together with a dominating bound on sets of finite measure forms a dominated FinMeasAdditive relation.

Русский

Отображение FinMeasAdditive с ограничением, доминирующим по мерам конечной меры, образует доминированное FinMeasAdditive.

LaTeX

$$DominatedFinMeasAdditive μ T C := FinMeasAdditive μ T ∧ ∀ s, MeasurableSet s → μ s < ∞ → ∥T s∥ ≤ C * μ.real s$$

Lean4

theorem zero {m : MeasurableSpace α} (μ : Measure α) (hC : 0 ≤ C) : DominatedFinMeasAdditive μ (0 : Set α → β) C :=
  by
  refine ⟨FinMeasAdditive.zero, fun s _ _ => ?_⟩
  rw [Pi.zero_apply, norm_zero]
  exact mul_nonneg hC toReal_nonneg

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