Commit 2024-07-14 15:55 9e5ed185

View on Github →

feat(UniformSpace/Cauchy): add lemmas about TotallyBounded (#13451)

Estimated changes

Modified Mathlib/Data/Set/Finite.lean

added theorem Set.exists_subset_image_finite_and

Modified Mathlib/Topology/Instances/Rat.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem Set.Finite.totallyBounded

added theorem Set.Subsingleton.totallyBounded

added theorem TotallyBounded.subset

added theorem totallyBounded_biUnion

added theorem totallyBounded_closure

modified theorem totallyBounded_empty

added theorem totallyBounded_iUnion

added theorem totallyBounded_insert

added theorem totallyBounded_sUnion

added theorem totallyBounded_singleton

deleted theorem totallyBounded_subset

added theorem totallyBounded_union

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added theorem totallyBounded_image_iff

modified theorem totallyBounded_preimage