English
If a ≤ c and b ∈ [a,c], the interval integrability on [a,c] follows from integrability on [a,b] and [b,c].
Русский
Если a ≤ c и b ∈ [a,c], интервальная интегрируемость на [a,c] следует из интегрируемости на [a,b] и [b,c].
LaTeX
$$$$\text{IntervalIntegrable}(f, μ, a, c) \iff \text{IntervalIntegrable}(f, μ, a, b) \wedge \text{IntervalIntegrable}(f, μ, b, c).$$$$
Lean4
theorem trans_iterate_Ico {a : ℕ → ℝ} {m n : ℕ} (hmn : m ≤ n)
(hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a <| k + 1)) : IntervalIntegrable f μ (a m) (a n) :=
by
revert hint
refine Nat.le_induction ?_ ?_ n hmn
· simp
· intro p hp IH h
exact (IH fun k hk => h k (Ico_subset_Ico_right p.le_succ hk)).trans (h p (by simp [hp]))