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.