Commit 2026-02-17 17:59 c66b8e24

View on Github →

feat(Topology/ContinuousMap/LocallyConstant): the range of toContinuousMapAlgHom separates points (#35221) ... in a totally separated space.

Estimated changes

Modified Mathlib/Topology/ContinuousMap/LocallyConstant.lean

added theorem LocallyConstant.separatesPoints_range_toContinuousMapAlgHom

added theorem LocallyConstant.toAddMonoidHom_toContinuousMapLinearMap

added theorem LocallyConstant.toLinearMap_toContinuousMapAlgHom