Theorems · Definition · functional analysis
ContinuousMapZero.id
{R : Type u_3} →
[inst : Zero R] → [inst_1 : TopologicalSpace R] → (s : Set R) → [inst_2 : Fact (0 ∈ s)] → ContinuousMapZero (↑s) RThe identity function as an element of C(s, R)₀ when 0 ∈ (s : Set R).
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroTopologicalSpaceFact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.Elemstatement · cited by 7,166
- Factstatement and proof · cited by 2,726
- ContinuousMapZerostatement · cited by 167
- ContinuousMap.idproof · cited by 73
- ContinuousMap.restrictproof · cited by 61
- Set.zeroOfFactMemstatement · cited by 14
Cited by25
Results whose statement or proof uses this declaration.
- cfcₙHom_idstatement · cited by 10
- ContinuousMapZero.induction_on_of_compactstatement and proof · cited by 4
- ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_idstatement · cited by 4
- ContinuousMapZero.adjoin_id_densestatement and proof · cited by 3
- cfcₙAux_idstatement · cited by 3
- cfcₙHom_eq_of_continuous_of_map_idstatement and proof · cited by 3
- range_cfcₙHom_leproof · cited by 2
- QuasispectrumRestricts.nonUnitalStarAlgHom_idstatement and proof · cited by 2
- cfcₙHomSuperset_idstatement · cited by 2
- ContinuousMapZero.elemental_eq_topstatement · cited by 2
- Commute.cfcₙHomproof · cited by 2
- continuous_cfcₙHomSuperset_leftproof · cited by 1