Commit 2025-04-21 23:31 26979609

View on Github →

feat: add versions of the Lebesgue number lemma (#22890) Add versions of the Lebesgue number lemma, for coverings by neighborhoods rather than by open subsets (in Topology/UniformSpace/Compact.lean). Add specializations of the Lebesgue number lemma for extended metric spaces (in Topology/EMetricSpace/Basic.lean).

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem lebesgue_number_lemma_of_emetric

added theorem lebesgue_number_lemma_of_emetric_nhds'

added theorem lebesgue_number_lemma_of_emetric_nhds

added theorem lebesgue_number_lemma_of_emetric_nhdsWithin'

added theorem lebesgue_number_lemma_of_emetric_nhdsWithin

added theorem lebesgue_number_lemma_of_emetric_sUnion

Modified Mathlib/Topology/UniformSpace/Compact.lean

added theorem lebesgue_number_lemma_nhds'

added theorem lebesgue_number_lemma_nhds

added theorem lebesgue_number_lemma_nhdsWithin'

added theorem lebesgue_number_lemma_nhdsWithin