congr_codiscreteWithin — Mathlib

English

If b belongs to [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

$$$$I(a,c) \text{ interval integrable} \iff I(a,b) \text{ and } I(b,c) \text{ interval integrable}.$$$$

Lean4

/-- Interval integrability is invariant when functions change along discrete sets. -/
theorem congr_codiscreteWithin {g : ℝ → ε} [NoAtoms μ] (h : f =ᶠ[codiscreteWithin (Ι a b)] g)
    (hf : IntervalIntegrable f μ a b) : IntervalIntegrable g μ a b :=
  hf.congr_ae (ae_restrict_le_codiscreteWithin measurableSet_Ioc h)

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