im — Mathlib · SciLib

English

The imaginary part of a complex measure is a signed measure mapping c to im(c).

Русский

Воображаемая часть комплексной меры — смешанная мера, отображающая c в im c.

LaTeX

$$im : ComplexMeasure α → SignedMeasure α$$

Lean4

/-- The imaginary part of a complex measure is a signed measure. -/
@[simps! apply]
def im : ComplexMeasure α →ₗ[ℝ] SignedMeasure α :=
  mapRangeₗ Complex.imCLM Complex.continuous_im

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