real — Mathlib

English

The real-valued version of a measure is defined by real μ(s) = (μ s).toReal.

Русский

Де-факто: вещественная версия меры задана как real μ(s) = (μ(s)).toReal.

LaTeX

$$MeasureTheory.Measure.real μ s = (μ s).toReal$$

Lean4

/-- The real-valued version of a measure. Maps infinite measure sets to zero. Use as `μ.real s`.
The API is developed in `Mathlib/MeasureTheory/Measure/Real.lean`. -/
protected def real {α : Type*} {m : MeasurableSpace α} (μ : Measure α) (s : Set α) : ℝ :=
  (μ s).toReal

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