Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-25 08:21 40f13709

View on Github →

chore(measure_theory/bochner_integration): rename/add lemmas, fix docstring (#4249)

  • add integral_nonneg assuming 0 ≤ f;
  • rename integral_nonpos_of_nonpos_ae to integral_nonpos_of_ae;
  • add integral_nonpos assuming f ≤ 0;
  • rename integral_mono to integral_mono_ae;
  • add integral_mono assuming f ≤ g;
  • (partially?) fix module docstring.

Estimated changes