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