mono_set_ae — Mathlib

English

If f is interval-integrable on [a,b] and Ι c d ≤ᵐ[μ] Ι a b, then f is interval-integrable on [c,d] under μ.

Русский

Если f интервал-интегрируема на [a,b] и Ιc d ≤ᵐ[μ] Ιa b, тогда f интервал-интегрируема на [c,d] относительно μ.

LaTeX

$$$\operatorname{IntervalIntegrable}(f,μ,a,b) \rightarrow (Ι c d ≤ᵐ[μ] Ι a b) \rightarrow \operatorname{IntervalIntegrable}(f,μ,c,d)$$$

Lean4

theorem mono_set_ae (hf : IntervalIntegrable f μ a b) (h : Ι c d ≤ᵐ[μ] Ι a b) : IntervalIntegrable f μ c d :=
  intervalIntegrable_iff.mpr <| hf.def'.mono_set_ae h

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