lintegral — Mathlib

English

If R is a star-structured space with continuity of star operation, the star on AEEqFun is defined pointwise via composition with star.

Русский

Если R — пространство со звездой и звезда непрерывна, то звезда на AEEqFun задаётся точечно через композицию со звездой.

LaTeX

$$instStarOfContinuousStar : Star (MeasureTheory.AEEqFun α R μ)$$

Lean4

/-- For `f : α → ℝ≥0∞`, define `∫ [f]` to be `∫ f` -/
def lintegral (f : α →ₘ[μ] ℝ≥0∞) : ℝ≥0∞ :=
  Quotient.liftOn' f (fun f => ∫⁻ a, (f : α → ℝ≥0∞) a ∂μ) fun _ _ => lintegral_congr_ae

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