Theorems · Definition · functional analysis

CompactlySupportedContinuousMap.toNNRealLinear

{α : Type u_2} →
  [inst : TopologicalSpace α] →
    (CompactlySupportedContinuousMap α ℝ →ₚ[ℝ] ℝ) → CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal

For a positive linear functional Λ : C_c(α, ℝ) → ℝ, define a ℝ≥0-linear map.

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

6 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace