Commit 2025-12-09 01:44 c25bbe0e

View on Github →

feat(Topology): basic properties of discrete sets (#32530)

Estimated changes

Modified Mathlib/Topology/DiscreteSubset.lean

added theorem IsDiscrete.eq_of_specializes

added theorem IsDiscrete.image

added theorem IsDiscrete.image_of_isOpenMap

added theorem IsDiscrete.image_of_isOpenMap_of_isOpen

added theorem IsDiscrete.of_nhdsWithin

added theorem IsDiscrete.preimage'

added theorem IsDiscrete.preimage

added theorem IsDiscrete.univ

added theorem IsEmbedding.isDiscrete_range

added theorem IsOpenMap.isDiscrete_range

added theorem Set.Subsingleton.isDiscrete

added theorem isDiscrete_iff_nhdsWithin

added theorem isDiscrete_univ_iff

Modified Mathlib/Topology/Separation/Basic.lean