Commit 2024-05-27 07:04 389c0ea5

View on Github →

feat: uniform structure on ContinuousMapZero (#12992) Also a bit of reorganization around the whole (short) file. This will be used for constructing non-unital functional calculi.

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

added theorem ContinuousMapZero.closedEmbedding_toContinuousMap

added theorem ContinuousMapZero.coe_add

added theorem ContinuousMapZero.coe_mul

added theorem ContinuousMapZero.coe_smul

added theorem ContinuousMapZero.coe_star

added theorem ContinuousMapZero.coe_zero

added theorem ContinuousMapZero.embedding_toContinuousMap

added theorem ContinuousMapZero.range_toContinuousMap

modified theorem ContinuousMapZero.toContinuousMap_injective

added theorem ContinuousMapZero.uniformEmbedding_toContinuousMap