mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(MeasureTheory): generalize `ae` to `OuterMeasureClass`

Open urkud opened this issue 9 months ago • 2 comments

  • Move definition and some lemmas from MeasureSpaceDef to OuterMeasure.AE.
  • Rename MeasureTheory.Measure.ae to MeasureTheory.ae.
  • Generalize the definition and theorems to [OuterMeasureClass _ _].

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.22Almost.20every.22.20on.20outer.20measures and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Order.20on.20measures/near/425729507

Open in Gitpod

urkud avatar May 19 '24 04:05 urkud