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_nhdsWithin'View on Github →