Theorem LocallyConstant.separatesPoints_range_toContinuousMapAlgHom

Modification history

2026-02-17 17:59

Mathlib/Topology/ContinuousMap/LocallyConstant.lean

feat(Topology/ContinuousMap/LocallyConstant): the range of `toContinuousMapAlgHom` separates points (#35221) …

Added LocallyConstant.separatesPoints_range_toContinuousMapAlgHom View on Github →