theorem Chapter11.not_integrable : Chapter9.BddOn Chapter9.f_9_3_21 ↑(BoundedInterval.Icc 0 1) ∧ ¬IntegrableOn Chapter9.f_9_3_21 (BoundedInterval.Icc 0 1)

Proposition 11.7.1