Commit 2024-03-05 05:13 b74ece72

View on Github →

chore(UniformSpace): move lemmas about compact sets together (#10783) Also add a Filter.HasBasis version of the Lebesgue number lemma, use it to golf IsCompact.nhdsSet_basis_uniformity, and use IsCompact.nhdsSet_basis_uniformity to golf lebesgue_number_of_compact_open.

Estimated changes

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

modified theorem IsCompact.nhdsSet_basis_uniformity

modified theorem lebesgue_number_lemma

modified theorem lebesgue_number_lemma_sUnion

modified theorem lebesgue_number_of_compact_open

added theorem lift'_comp_uniformity