integral_non_aestronglyMeasurable_of_le

English

If a ≤ b and f is not AEStronglyMeasurable on μ restricted to Ioc a b, then the interval integral is zero.

Русский

Если a ≤ b и f не AEStronglyMeasurable на μ|_{Ioc a b}, то интервальный интеграл равен нулю.

LaTeX

$$$a \\le b \\Rightarrow Not (AEStronglyMeasurable f (μ|_{Ioc a b})) \\Rightarrow \\int x in a..b f(x) ∂μ = 0$$$

Lean4

theorem integral_non_aestronglyMeasurable_of_le (h : a ≤ b) (hf : ¬AEStronglyMeasurable f (μ.restrict (Ioc a b))) :
    ∫ x in a..b, f x ∂μ = 0 :=
  integral_non_aestronglyMeasurable <| by rwa [uIoc_of_le h]

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