Theorem IsEmbedding.isDiscrete_range

Modification history

2026-03-30 20:13
Mathlib/Topology/DiscreteSubset.lean
feat(Topology): weaken assumption is ```IsDiscrete.image``` (#37378) …
Deleted IsEmbedding.isDiscrete_rangeView on Github →
2025-12-09 01:44
Mathlib/Topology/DiscreteSubset.lean
feat(Topology): basic properties of discrete sets (#32530)
Added IsEmbedding.isDiscrete_rangeView on Github →