Commit 2024-08-26 06:52 d011eb15

View on Github →

feat(Measure/Typeclasses): prove ≪ both ways (#16146)

  • Rename exists_absolutelyContinuous_isFiniteMeasure to exists_isFiniteMeasure_absolutelyContinuous to match the statement.
  • Prove ν ≪ μ, not only μ ≪ ν.
  • Turn the old lemma into a deprecated alias.

Estimated changes