intervalIntegrable_of_integral_ne_zero

English

If the interval integral is not zero, then the function is interval integrable on [a,b].

Русский

Если интервальный интеграл не ноль, то функция интервално интегрируема на [a,b].

LaTeX

$$$Ne (\\int x in a..b, f x ∂μ) 0 \\Rightarrow IntervalIntegrable f μ a b$$$

Lean4

theorem intervalIntegrable_of_integral_ne_zero {a b : ℝ} {f : ℝ → E} {μ : Measure ℝ} (h : (∫ x in a..b, f x ∂μ) ≠ 0) :
    IntervalIntegrable f μ a b :=
  not_imp_comm.1 integral_undef h

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