measurableLEEval — Mathlib

English

measurableLEEval(μ, ν) is the set of all numbers ∫ f dμ that arise from f ∈ measurableLE(μ, ν).

Русский

measurableLEEval(μ, ν) — множество значений ∫ f dμ, где f ∈ measurableLE(μ, ν).

LaTeX

$$$$ measurableLEEval(\\mu, \\nu) = \\{ \\int f \\, d\\mu \\, \\mid \\ f \\in \\mathrm{measurableLE}(\\mu, \\nu) \\}. $$$$

Lean4

/-- `measurableLEEval μ ν` is the set of `∫⁻ x, f x ∂μ` for all `f ∈ measurableLE μ ν`. -/
def measurableLEEval (μ ν : Measure α) : Set ℝ≥0∞ :=
  (fun f : α → ℝ≥0∞ ↦ ∫⁻ x, f x ∂μ) '' measurableLE μ ν

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