Commit 2026-01-13 23:44 26e1e450

View on Github →

feat(Topology/UniformSpace): generalize TotallyBounded to filters (#33128) Some of these generalizations will be useful for showing the completeness of TopologicalSpace.Compacts in a non-metrizable setting.

Estimated changes

Modified Mathlib/Data/Rel.lean

added theorem SetRel.image_eq_biUnion

added theorem SetRel.preimage_eq_biUnion

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem Filter.HasBasis.filter_totallyBounded_iff

added theorem Filter.TotallyBounded.exists_clusterPt

added theorem Filter.TotallyBounded.exists_subset_of_mem

added theorem Filter.TotallyBounded.isCompact_setOf_clusterPt

added theorem Filter.TotallyBounded.map

added theorem Filter.TotallyBounded.mono

added theorem Filter.TotallyBounded.sup

added theorem Filter.TotallyBounded.totallyBounded_setOf_clusterPt

added theorem Filter.totallyBounded_biSup

added theorem Filter.totallyBounded_bot

added theorem Filter.totallyBounded_iSup

added theorem Filter.totallyBounded_principal_iff

added theorem Filter.totallyBounded_sup

modified theorem TotallyBounded.closure

added theorem Ultrafilter.cauchy_of_totallyBounded'

added theorem totallyBounded_sSup

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added theorem Filter.totallyBounded_comap

added theorem Filter.totallyBounded_map_iff