Theorem lebesgue_number_lemma_nhdsWithin

Modification history

2025-04-21 23:31
Mathlib/Topology/UniformSpace/Compact.lean
feat: add versions of the Lebesgue number lemma (#22890) …
Added lebesgue_number_lemma_nhdsWithinView on Github →