Commit 2024-10-12 07:45 47521133

View on Github →

chore(MeasureTheory/Integral/SetIntegral): fix lemma names (#17658) Rename:

  • integral_empty -> setIntegral_empty
  • integral_union -> setIntegral_union
  • integral_univ -> setIntegral_univ
  • setIntegral_congr -> setIntegral_congr_fun
  • setIntegral_congr₀ -> setIntegral_congr_fun₀
  • setLIntegral_congr_set_ae -> setIntegral_congr_set From PFR

Estimated changes