Commit 2025-02-03 17:10 25490574

View on Github →

feat(Topology/ContinuousMap/CompactlySupported): turn a positive Real-linear functional into a NNReal-linear functional (#20257) Define toNNRealLinear that maps positive Real-linear functionals to NNReal-linear functionals and prove that it is injective.

Estimated changes

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

added theorem CompactlySupportedContinuousMap.coe_toRealLinearMap

added theorem CompactlySupportedContinuousMap.nnrealPart_sub_nnrealPart_neg

added theorem CompactlySupportedContinuousMap.toNNRealLinear_apply

added theorem CompactlySupportedContinuousMap.toNNRealLinear_inj

added theorem CompactlySupportedContinuousMap.toRealLinearMap_apply

added theorem CompactlySupportedContinuousMap.toRealLinearMap_apply_apply

added theorem CompactlySupportedContinuousMap.toReal_add

added theorem CompactlySupportedContinuousMap.toReal_apply

added theorem CompactlySupportedContinuousMap.toReal_nonneg

added theorem CompactlySupportedContinuousMap.toReal_smul

Modified Mathlib/Topology/Instances/NNReal/Defs.lean

added theorem NNReal.coeNNRealReal_zero