Commit 2025-01-22 09:03 c971e4ff
View on Github →feat: a non-zero constant function is integrable iff the measure is finite (#20914)
The situation here is that I want to case on IsFiniteMeasure μ
, and in the negative branch I want to get ¬ Integrable (fun _ ↦ c) μ
. The current lemma integrable_const_iff
is not very useful for that.
From my PhD (LeanCamCombi)