re — Mathlib · SciLib

English

The real part of a complex measure is a signed measure mapping c to re(c).

Русский

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

LaTeX

$$re : ComplexMeasure α → SignedMeasure α$$

Lean4

/-- The real part of a complex measure is a signed measure. -/
@[simps! apply]
def re : ComplexMeasure α →ₗ[ℝ] SignedMeasure α :=
  mapRangeₗ Complex.reCLM Complex.continuous_re

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