Theorems · Definition · general topology

ContinuousMap.mkD

{α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (α → β) → C(α, β) → C(α, β)

Interpret f : α → β as an element of C(α, β), falling back to the default value default : C(α, β) if f is not continuous. 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 for almost every i, you can write the C(α, β)-valued integral "∫ i, f i" as ∫ i, ContinuousMap.mkD (f i) 0.

Defined in

Mathlib.Topology.ContinuousMap.Basic

Cited by

28 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace