mathlib

e94e5c08 - feat(topology/uniform_space/basic): uniform continuity from/to an infimum of uniform spaces (#14892)

feat(topology/uniform_space/basic): uniform continuity from/to an infimum of uniform spaces (#14892) This adds uniform versions of various topological lemmas about continuity from/to infimas of topological spaces Co-authored-by: Eric Wieser <wieser.eric@gmail.com>