Commit 2026-05-04 18:51 a62d5cd7

View on Github →

refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/LpSeminorm/Count (#38878)

  • rewrites eLpNorm_count_lt_top_of_lt using eLpNorm_mono_enorm with the finite supremum bound instead of splitting on the definition of eLpNorm
  • closes the finiteness goal with memLp_const_enorm rather than a manual lintegral_count computation Extracted from #38104 Open in Gitpod

Estimated changes