Theorem IsInducing.isDiscrete_range

Modification history

2026-06-22 16:23
Mathlib/Topology/DiscreteSubset.lean
chore(Topology): namespace lemmas around `IsInducing`, `IsQuotientMap` etc (#40891) …
Deleted IsInducing.isDiscrete_rangeView on Github →
2026-03-30 20:13
Mathlib/Topology/DiscreteSubset.lean
feat(Topology): weaken assumption is ```IsDiscrete.image``` (#37378) …
Added IsInducing.isDiscrete_rangeView on Github →