Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-11 14:51 25dded2d

View on Github →

chore(measure_theory/bochner_integration): make proofs shorter (#1871)

  • More consistent use of the dot notation
  • Revert "More consistent use of the dot notation" This reverts commit 854a499a9be105b42ca486eb25593a2379b07404.
  • Revert "Revert "More consistent use of the dot notation"" This reverts commit 57aaf22695c031fc8dcc581110cc9d1ac397f695.
  • fix things

Estimated changes

modified theorem measure_theory.integral_add
modified theorem measure_theory.integral_eq
modified theorem measure_theory.integral_sub
added theorem measurable.coe_nnnorm
added theorem measurable.dist
added theorem measurable.edist
added theorem measurable.nndist
added theorem measurable.nnnorm
added theorem measurable.norm
added theorem measurable.smul'
added theorem measurable.smul
added theorem measurable_dist
added theorem measurable_edist
added theorem measurable_nndist
added theorem measurable_nnnorm
added theorem measurable_norm
added theorem measurable_smul_iff
modified def measure_theory.l1
added theorem measurable_zero