Theorem ContinuousMapZero.toContinuousMap_id

Modification history

2025-09-18 15:32
Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
refactor: switch to using `Fact (0 ∈ s)` for `ContinuousMapZero.id` (#29563) …
Modified ContinuousMapZero.toContinuousMap_idView on Github →
2024-05-29 14:23
Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean
feat: add more features to `ContinuousMapZero` (#13323) …
Added ContinuousMapZero.toContinuousMap_idView on Github →