Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-05 17:46 8786ea6d

View on Github →

refactor(measure_theory/set_integral): move set integral into namespace set and add some lemmas (#1950)

  • move set integral into namespace set and add some lemmas
  • Update bochner_integration.lean
  • better theorem names
  • Update set_integral.lean
  • Update set_integral.lean

Estimated changes

modified theorem integrable_on.smul
modified def integrable_on
modified theorem integrable_on_congr_ae
modified theorem integrable_on_empty
modified theorem integral_on_congr
added theorem integral_on_nonneg
added theorem integral_on_nonpos
added theorem integral_on_undef
modified def measurable_on
modified theorem measurable_on_empty
modified theorem measurable_on_singleton
deleted theorem measurable_on_univ