Theorem CompactlySupportedContinuousMap.nnrealPart_apply

Modification history

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