toSignedMeasure_eq_toSignedMeasure_iff

English

Two finite measures have equal signed measures if and only if the measures themselves are equal.

Русский

У двух конечных мер равны их подписанные меры тогда и только тогда, когда сами меры равны.

LaTeX

$$$μ.toSignedMeasure = ν.toSignedMeasure \iff μ = ν$$$

Lean4

theorem toSignedMeasure_eq_toSignedMeasure_iff {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · ext1 i hi
    have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]
    rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
      measureReal_eq_measureReal_iff] at this
  · congr

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