Commit 2026-08-24 15:09 2e7bad0d

View on Github →

feat: variants of Measurable.oneLePart and related lemmas (#41322) This PR does 3 things:

  • add lemmas about measurability of oneLePart, leOnePart, posPart and negPart of functions
  • generalize the existing lemmas from Group to DivInvMonoid (and AddGroup to SubNegMonoid, which covers EReal).
  • use notation for those positive and negative parts instead of their full names.

Estimated changes

modified theorem measurable_leOnePart
modified theorem measurable_oneLePart