mono_set — Mathlib

English

If f is interval-integrable with μ on [a,b], and [c,d] ⊆ [a,b], then f is interval-integrable with μ on [c,d].

Русский

Если f интервал-интегрируема по μ на [a,b], и [c,d] ⊆ [a,b], то она интервал-интегрируема на [c,d].

LaTeX

$$$\operatorname{IntervalIntegrable}(f,μ,a,b) \Rightarrow [[c,d]] ⊆ [[a,b]] \Rightarrow \operatorname{IntervalIntegrable}(f,μ,c,d)$$$

Lean4

theorem mono_set (hf : IntervalIntegrable f μ a b) (h : [[c, d]] ⊆ [[a, b]]) : IntervalIntegrable f μ c d :=
  hf.mono h le_rfl

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