Theorems · Definition · functional analysis

ContinuousMapZero.mkD

{X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero R] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] → [inst_3 : Zero X] → (X → R) → ContinuousMapZero X R → ContinuousMapZero X R

Interpret f : α → β as an element of C(α, β)₀, falling back to the default value default : C(α, β)₀ if f is not continuous or does not map 0 to 0. This is mainly intended to be used for C(α, β)₀-valued integration. For example, if a family of functions f : ι → α → β satisfies that f i is continuous and maps 0 to 0 for almost every i, you can write the C(α, β)₀-valued integral "∫ i, f i" as ∫ i, ContinuousMapZero.mkD (f i) 0.

Defined in

Mathlib.Topology.ContinuousMap.ContinuousMapZero

Cited by

21 results in Mathlib

Foundations

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

Assumes

ZeroTopologicalSpaceTopologicalSpaceZero