toSignedMeasure_le_toSignedMeasure_iff

English

The order on measures corresponds to the order on their signed measures via the toSignedMeasure map; i.e., μ.toSignedMeasure ≤ ν.toSignedMeasure iff μ ≤ ν.

Русский

Порядок по мерoм отражается через отображение в сигнальные меры: μ^{toSignedMeasure} ≤ ν^{toSignedMeasure} тогда и только тогда, когда μ ≤ ν.

LaTeX

$$$\mu^{\mathrm{toSignedMeasure}} \le \nu^{\mathrm{toSignedMeasure}} \iff \mu \le \nu$$$

Lean4

theorem toSignedMeasure_le_toSignedMeasure_iff : μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν :=
  by
  rw [Measure.le_iff, VectorMeasure.le_iff]
  congrm ∀ s, (hs : MeasurableSet s) → ?_
  simp_rw [toSignedMeasure_apply_measurable hs, real_def]
  apply ENNReal.toReal_le_toReal <;> finiteness

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