Theorems · Definition · functional analysis
CompactlySupportedContinuousMap.toContinuousMap
{α : Type u_5} →
{β : Type u_6} →
[inst : TopologicalSpace α] →
[inst_1 : Zero β] → [inst_2 : TopologicalSpace β] → CompactlySupportedContinuousMap α β → C(α, β)- Cited by
- 10 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- ContinuousMapstatement · cited by 2,491
- CompactlySupportedContinuousMapstatement and proof · cited by 134
Cited by11
Results whose statement or proof uses this declaration.
- CompactlySupportedContinuousMap.nnrealPartproof · cited by 15
- CompactlySupportedContinuousMap.integrableproof · cited by 9
- CompactlySupportedContinuousMap.hasCompactSupport'statement · cited by 4
- isCompact_setOfPred_finiteMeasure_le_of_compactSpaceproof · cited by 3
- contentRegular_rieszContentproof · cited by 3
- CompactlySupportedContinuousMap.exists_add_of_leproof · cited by 2
- rieszContentAux_unionproof · cited by 2
- CompactlySupportedContinuousMap.coe_toContinuousMapstatement · cited by 0
- RealRMK.exists_open_approxproof · cited by 0
- RealRMK.range_cut_partitionproof · cited by 0
- CompactlySupportedContinuousMap.toContinuousMap_compLeftstatement · cited by 0