def' — Mathlib

English

If f is IntervalIntegrable and f equals g almost everywhere on Ι(a,b), then g is IntervalIntegrable as well.

Русский

Если f интервал-интегрируема и f равно g почти наверняка на Ι(a,b), то и g интервал-интегрируема.

LaTeX

$$$$\text{IntervalIntegrable}(f,μ,a,b) \wedge f =_{μ|_{Ι(a,b)}} g \Rightarrow \text{IntervalIntegrable}(g,μ,a,b).$$$$

Lean4

/-- If a function is interval integrable with respect to a given measure `μ` on `a..b` then
  it is integrable on `uIoc a b` with respect to `μ`. -/
theorem def' (h : IntervalIntegrable f μ a b) : IntegrableOn f (Ι a b) μ :=
  intervalIntegrable_iff.mp h

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