im_toComplexMeasure — Mathlib

English

The imaginary part map is compatible with ComplexMeasure formation from a SignedMeasure pair.

Русский

Мнимая часть совместима с образованием комплексной меры из пары смешанных мер.

LaTeX

$$im_toComplexMeasure : SignedMeasure α → SignedMeasure α → ComplexMeasure α$$

Lean4

theorem _root_.MeasureTheory.SignedMeasure.im_toComplexMeasure (s t : SignedMeasure α) :
    ComplexMeasure.im (SignedMeasure.toComplexMeasure s t) = t :=
  rfl

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