Commit 2026-05-14 02:57 62263833

View on Github →

feat(DiscreteSubset): review API, add lemmas about compact sets (#39336)

Migrate some lemmas from DiscreteTopology (_ : Set _) to IsDiscrete.
Generalize mem_codiscrete_subtype_iff_mem_codiscreteWithin to a topological embedding.
Add lemmas about codiscreteWithin for a compact set and codiscrete for a compact space.

Estimated changes

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

Modified Mathlib/Analysis/Complex/JensenFormula.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/Topology/DiscreteSubset.lean

deleted theorem Filter.codiscreteWithin.mono

added theorem Filter.codiscreteWithin_mono

added theorem IsCompact.codiscreteWithin_eq

added theorem IsCompact.cofinite_inf_le_codiscreteWithin

added theorem IsCompact.finite_diff_of_mem_codiscreteWithin

added theorem IsDiscrete.biUnion

added theorem IsDiscrete.biUnion_finset

added theorem IsDiscrete.iUnion

added theorem IsDiscrete.union

added theorem Topology.IsEmbedding.image_mem_codiscreteWithin

added theorem Topology.IsEmbedding.image_mem_codiscreteWithin_range

added theorem codiscreteWithin_le_codiscrete_inf_principal

added theorem codiscrete_eq_cofinite

added theorem cofinite_le_codiscrete