Commit 2025-11-25 20:26 1993fc2f

View on Github →

feat(Topology/Constructions): IsDiscrete predicate on sets (#30349) Define an IsDiscrete predicate on sets in a topological space (which is equivalent to DiscreteTopology for the corresponding subtype).

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Algebra/Module/ZLattice/Summable.lean

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Topology.lean

Modified Mathlib/NumberTheory/NumberField/Units/Regulator.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean

Modified Mathlib/Topology/Algebra/Field.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

modified theorem Subgroup.tendsto_coe_cofinite_of_discrete

Modified Mathlib/Topology/Compactness/Compact.lean

modified theorem IsCompact.finite

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/Constructions.lean

added theorem DiscreteTopology.isDiscrete

added theorem IsDiscrete.mono

added structure IsDiscrete

added theorem SetLike.isDiscrete_iff_discreteTopology

added theorem isDiscrete_iff_discreteTopology

Modified Mathlib/Topology/DiscreteSubset.lean

deleted theorem IsClosed.tendsto_coe_cofinite_of_discreteTopology

added theorem IsClosed.tendsto_coe_cofinite_of_isDiscrete

deleted theorem discreteTopology_of_codiscreteWithin

added theorem isDiscrete_iff_forall_exists_isOpen

added theorem isDiscrete_iff_nhdsNE

added theorem isDiscrete_of_codiscreteWithin

Modified Mathlib/Topology/Instances/ZMultiples.lean

Modified Mathlib/Topology/IsLocalHomeomorph.lean

added theorem IsLocalHomeomorphOn.isDiscrete_image_iff

added theorem IsLocalHomeomorphOn.isDiscrete_of_image

Modified Mathlib/Topology/LocallyFinsupp.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

modified theorem Metric.finite_isBounded_inter_isClosed

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

modified theorem Metric.exists_ball_inter_eq_singleton_of_mem_discrete

modified theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete

Modified Mathlib/Topology/Separation/Basic.lean

added theorem Set.Finite.isDiscrete

modified theorem disjoint_nhdsWithin_of_mem_discrete

modified theorem isOpen_inter_eq_singleton_of_mem_discrete

modified theorem nhdsWithin_of_mem_discrete

modified theorem nhds_inter_eq_singleton_of_mem_discrete

modified theorem singleton_mem_nhdsWithin_of_mem_discrete