mono — Mathlib

English

If f is interval-integrable with respect to ν on [a,b], and μ ≤ ν, then f is interval-integrable with respect to μ on [c,d] whenever [c,d] ⊆ [a,b] (in the interval sense).

Русский

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

LaTeX

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

Lean4

theorem mono (hf : IntervalIntegrable f ν a b) (h1 : [[c, d]] ⊆ [[a, b]]) (h2 : μ ≤ ν) : IntervalIntegrable f μ c d :=
  intervalIntegrable_iff.mpr <| hf.def'.mono (uIoc_subset_uIoc_of_uIcc_subset_uIcc h1) h2

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