toComplexMeasure_to_signedMeasure

English

For a complex measure c, the map from its real and imaginary parts recovers c: SignedMeasure.toComplexMeasure (ComplexMeasure.re c) (ComplexMeasure.im c) = c.

Русский

Для комплексной меры c отображение по ее реальной и мнимой частям восстанавливает c: toComplexMeasure(re c, im c) = c.

LaTeX

$$SignedMeasure.toComplexMeasure (ComplexMeasure.re c) (ComplexMeasure.im c) = c$$

Lean4

theorem toComplexMeasure_to_signedMeasure (c : ComplexMeasure α) :
    SignedMeasure.toComplexMeasure (ComplexMeasure.re c) (ComplexMeasure.im c) = c :=
  rfl

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