Commit 2023-12-27 20:59 521f71ff

View on Github →

feat: misc lemmas on uniform spaces (#9305)

Estimated changes

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformSpace.ball_mem_nhdsWithin

added theorem nhdsWithin_eq_comap_uniformity

added theorem nhdsWithin_eq_comap_uniformity_of_mem

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added theorem UniformInducing.uniformContinuousOn_iff