Theorems · Definition · functional analysis
ContinuousMapZero.toNNReal
{X : Type u_1} → [inst : TopologicalSpace X] → [inst_1 : Zero X] → ContinuousMapZero X ℝ → ContinuousMapZero X NNRealThis map sends f : C(X, ℝ) to Real.toNNReal ∘ f, bundled as a continuous map C(X, ℝ≥0).
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- NNRealstatement · cited by 4,310
- ContinuousMap.compproof · cited by 181
- ContinuousMapZerostatement and proof · cited by 167
- toContinuousMapproof · cited by 99
- ContinuousMap.realToNNRealproof · cited by 44
Cited by10
Results whose statement or proof uses this declaration.
- NonUnitalStarAlgHom.realContinuousMapZeroOfNNRealproof · cited by 4
- ContinuousMapZero.toNNReal_smulstatement · cited by 1
- NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toRealproof · cited by 1
- NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_applystatement · cited by 1
- ContinuousMapZero.continuous_toNNRealstatement and proof · cited by 1
- ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eqstatement and proof · cited by 0
- ContinuousMapZero.toNNReal_neg_smulstatement and proof · cited by 0
- ContinuousMapZero.toContinuousMapHom_toNNRealstatement · cited by 0
- ContinuousMapZero.toNNReal_add_add_neg_add_neg_eqstatement and proof · cited by 0
- ContinuousMapZero.toNNReal_applystatement · cited by 0