setAverage_sub_setAverage — Mathlib

English

If μ is finite and f is integrable, then the average over μ restricted to s lies in the segment between the averages over s and sᶜ.

Русский

Если μ конечна и f интегрируема, то среднее по μ|s лежит в сегменте между средними по s и по sᶜ.

LaTeX

$$$\operatorname{average}_{\mu|_s} f \in [ \operatorname{average}_{\mu|_s} f, \operatorname{average}_{\mu|_{s^c}} f ]$$$

Lean4

theorem setAverage_sub_setAverage (hs : μ s ≠ ∞) (f : α → E) : ∫ x in s, f x - ⨍ a in s, f a ∂μ ∂μ = 0 :=
  haveI : Fact (μ s < ∞) := ⟨lt_top_iff_ne_top.2 hs⟩
  integral_sub_average _ _

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