setLAverage_lt_top — Mathlib

English

If the restricted lintegral is not top, then the laverage is below top.

Русский

Если ограниченный интеграл не достигает верхней границы, то среднее меньше верхней границы.

LaTeX

$$$\\text{if } \\lintegral_{\\mu|s} f ≠ \\top \\Rightarrow \\laverage_{\\mu|s} f < \\top$$$

Lean4

theorem setLAverage_lt_top : ∫⁻ x in s, f x ∂μ ≠ ∞ → ⨍⁻ x in s, f x ∂μ < ∞ :=
  laverage_lt_top

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