Theorem exists_continuous_add_one_of_isCompact_nnreal

Modification history

2024-12-17 01:35
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean
feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is indeed a content for `NNReal` (#18775) …
Added exists_continuous_add_one_of_isCompact_nnrealView on Github →