intervalIntegrable_congr_codiscreteWithin

English

From interval integrability, one obtains integrability on the oriented interval Ι(a,b).

Русский

Из интервальной интегрируемости следует интегрируемость на ориентированном интервале Ι(a,b).

LaTeX

$$$$\text{IntervalIntegrable}(f, μ, a, b) \Rightarrow \text{IntegrableOn}(f, Ι(a,b), μ).$$$$

Lean4

/-- Interval integrability is invariant when functions change along discrete sets. -/
theorem intervalIntegrable_congr_codiscreteWithin {g : ℝ → ε} [NoAtoms μ] (h : f =ᶠ[codiscreteWithin (Ι a b)] g) :
    IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b :=
  ⟨(IntervalIntegrable.congr_codiscreteWithin h ·), (IntervalIntegrable.congr_codiscreteWithin h.symm ·)⟩

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