withDensity_mono — Mathlib

English

If f ≤ᵐ μ g, then μ.withDensity f ≤ μ.withDensity g.

Русский

Если f ≤ᵐ μ g, тогда μ.withDensity f ≤ μ.withDensity g.

LaTeX

$$$f \leq_{\mu}^{\mathrm{ae}} g \Rightarrow \mu.withDensity f \le \mu.withDensity g$$$

Lean4

theorem withDensity_mono {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ[μ] g) : μ.withDensity f ≤ μ.withDensity g :=
  by
  refine le_iff.2 fun s hs ↦ ?_
  rw [withDensity_apply _ hs, withDensity_apply _ hs]
  refine setLIntegral_mono_ae' hs ?_
  filter_upwards [hfg] with x h_le using fun _ ↦ h_le

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