Theorems · Definition · functional analysis

CompactlySupportedContinuousMap.toRealPositiveLinear

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

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

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpace