integral_pos_of_integrable_nonneg_nonzero

English

If f is integrable and nonnegative and nonzero at some point, the integral is positive.

Русский

Если f интегрируема и неотрицательна и не равна нулю на некоторой точке, то интеграл положителен.

LaTeX

$$$\\displaystyle \\int f \\, d\\mu > 0$ under the stated conditions$$

Lean4

theorem integral_pos_of_integrable_nonneg_nonzero [TopologicalSpace α] [Measure.IsOpenPosMeasure μ] {f : α → ℝ} {x : α}
    (f_cont : Continuous f) (f_int : Integrable f μ) (f_nonneg : 0 ≤ f) (f_x : f x ≠ 0) : 0 < ∫ x, f x ∂μ :=
  (integral_pos_iff_support_of_nonneg f_nonneg f_int).2 (IsOpen.measure_pos μ f_cont.isOpen_support ⟨x, f_x⟩)

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