mono — Mathlib

English

If f is integrable on t with respect to ν, and s ⊆ t, and μ ≤ ν, then f is integrable on s with μ.

Русский

Если f интегрируема на t по ν, и s ⊆ t, и μ ≤ ν, то f интегрируема на s по μ.

LaTeX

$$$\mathrm{IntegrableOn}(f,t,\nu) \to s \subseteq t \to \mu \le \nu \to \mathrm{IntegrableOn}(f,s,\mu)$$$

Lean4

theorem mono (h : IntegrableOn f t ν) (hs : s ⊆ t) (hμ : μ ≤ ν) : IntegrableOn f s μ :=
  h.mono_measure <| Measure.restrict_mono hs hμ

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