Theorem lebesgue_number_lemma_of_emetric_nhdsWithin

Modification history

2026-08-13 16:41
Mathlib/Topology/EMetricSpace/Basic.lean
feat(Topology): generalize basic files to `Weak(Pseudo)EMetricSpace` (#42688) …
Modified lebesgue_number_lemma_of_emetric_nhdsWithinView on Github →
2025-04-21 23:31
Mathlib/Topology/EMetricSpace/Basic.lean
feat: add versions of the Lebesgue number lemma (#22890) …
Added lebesgue_number_lemma_of_emetric_nhdsWithinView on Github →