re_toComplexMeasure — Mathlib

English

The real part map is compatible with taking ComplexMeasure of a SignedMeasure.

Русский

Реальная часть совместима с преобразованием через ComplexMeasure для пары SignedMeasure.

LaTeX

$$re_toComplexMeasure : SignedMeasure α → SignedMeasure α → ComplexMeasure α$$

Lean4

theorem _root_.MeasureTheory.SignedMeasure.re_toComplexMeasure (s t : SignedMeasure α) :
    ComplexMeasure.re (SignedMeasure.toComplexMeasure s t) = s :=
  rfl

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