mono_measure — Mathlib

English

If f is interval-integrable with ν, and μ ≤ ν, then f is interval-integrable on a subinterval with the same μ.

Русский

Если f интервал-интегрируема по ν, и μ ≤ ν, то f интервал-интегрируема на подпериоде с тем же μ.

LaTeX

$$$\operatorname{IntervalIntegrable}(f,ν,a,b) \rightarrow μ ≤ ν \rightarrow \operatorname{IntervalIntegrable}(f,μ,a,b)$$$

Lean4

theorem mono_measure (hf : IntervalIntegrable f ν a b) (h : μ ≤ ν) : IntervalIntegrable f μ a b :=
  hf.mono Subset.rfl h

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