Commit 2024-06-22 09:56 eb89176f

View on Github →

feat(*): add lemmas about (_ : UniformSpace _) = ⊥ (#13481)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem DiscreteTopology.of_forall_le_norm'

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

added theorem DiscreteTopology.of_forall_le_dist

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformSpace.uniformSpace_eq_bot