zero_le_toSignedMeasure — Mathlib

English

0 ≤ μ.toSignedMeasure for any finite μ; hence μ.toSignedMeasure is nonnegative.

Русский

0 ≤ μ.toSignedMeasure для любой конечной μ; следовательно, μ.toSignedMeasure неотрицательна.

LaTeX

$$$ 0 \\le \\mu^{\\mathrm{toSignedMeasure}} $$$

Lean4

theorem zero_le_toSignedMeasure : 0 ≤ μ.toSignedMeasure :=
  by
  rw [← le_restrict_univ_iff_le]
  refine restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => ?_
  simp only [VectorMeasure.coe_zero, Pi.zero_apply, Measure.toSignedMeasure_apply_measurable hj₁, measureReal_nonneg]

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