Commit 2026-03-30 20:13 5c46c7d3

View on Github →

feat(Topology): weaken assumption is IsDiscrete.image (#37378) Credit goes to @erdOne at MRB. :)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

Modified Mathlib/Topology/DiscreteSubset.lean

modified theorem IsDiscrete.image

deleted theorem IsEmbedding.isDiscrete_range

added theorem IsInducing.isDiscrete_range