Commit 2024-02-20 17:52 8afb4109

View on Github →

chore(UniformSpace): golf (#10627) Golf the instance for UniformSpace (α ⊕ β) using the ofNhdsEqComap constructor.

Estimated changes

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

modified theorem Sum.uniformity

deleted def UniformSpace.Core.sum

deleted theorem isOpen_of_uniformity_sum_aux

deleted theorem uniformity_sum_of_isOpen_aux