English
An interval integrable function is one that is integrable on both subintervals (a, b] and (b, a].
Русский
Интервально интегрируемая функция — та, которая интегрируема на обоих подотрезках (a, b] и (b, a].
LaTeX
$$$$\text{IntervalIntegrable}(f,\mu,a,b) := (\text{IntegrableOn}(f,(a,b],μ)\;\land\;\text{IntegrableOn}(f,(b,a],μ)).$$$$
Lean4
/-- A function `f` is called *interval integrable* with respect to a measure `μ` on an unordered
interval `a..b` if it is integrable on both intervals `(a, b]` and `(b, a]`. One of these
intervals is always empty, so this property is equivalent to `f` being integrable on
`(min a b, max a b]`. -/
def IntervalIntegrable (f : ℝ → ε) (μ : Measure ℝ) (a b : ℝ) : Prop :=
IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ
