trans_iff — Mathlib

English

If b ∈ [a,c], then IntervalIntegrable on [a,c] is equivalent to the conjunction of IntervalIntegrable on [a,b] and [b,c].

Русский

Если b принадлежит [a,c], тогда интервальная интегрируемость на [a,c] эквивалентна объединению [a,b] и [b,c].

LaTeX

$$$$\text{IntervalIntegrable}(f, μ, a, c) \iff \left(\text{IntervalIntegrable}(f, μ, a, b) \land \text{IntervalIntegrable}(f, μ, b, c)\right)$$$$

Lean4

theorem trans_iff (h : b ∈ [[a, c]]) :
    IntervalIntegrable f μ a c ↔ IntervalIntegrable f μ a b ∧ IntervalIntegrable f μ b c := by
  simp only [intervalIntegrable_iff, ← integrableOn_union, uIoc_union_uIoc h]

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