lintegral_mono_fun — Mathlib

English

If f ≤ g as simple functions, then f.lintegral μ ≤ g.lintegral μ.

Русский

Если f ≤ g как простые функции, то f.lintegral μ ≤ g.lintegral μ.

LaTeX

$$$f \\le g \\implies f.lintegral(μ) \\le g.lintegral(μ)$$$

Lean4

theorem lintegral_mono_fun {f g : α →ₛ ℝ≥0∞} (h : f ≤ g) : f.lintegral μ ≤ g.lintegral μ :=
  by
  refine Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h
  calc
    f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
    _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ :=
      by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left

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