Commit 2026-08-11 14:44 5d488cb2

View on Github →

refactor: reorganize Topology/EMetricSpace/Defs to generalise basic results (#40510) This PR reorganizes the Topology/EMetricSpace/Defs so that various results that previously only held for PseudoEMetricSpace now also hold for WeakPseudoEMetricSpace (in particular, ENNReal). This is a necessary stepping stone to generalise many definitions and theorems to WeakPseudoEMetricSpace.

Estimated changes

modified theorem EMetric.isOpen_iff
modified theorem EMetric.mem_nhdsWithin_iff
modified theorem EMetric.mem_nhds_iff
modified theorem EMetric.nhds_eq
modified def Metric.closedEBall
modified theorem Metric.closedEBall_mem_nhds
modified theorem Metric.closedEBall_top
modified def Metric.eball
modified theorem Metric.eball_mem_nhds
modified theorem Metric.eball_zero
modified theorem Metric.isOpen_eball
modified theorem Metric.mem_closedEBall
modified theorem Metric.mem_eball
modified theorem Metric.nhds_basis_eball
modified theorem Metric.pos_of_mem_eball
deleted theorem MulOpposite.edist_op
deleted theorem MulOpposite.edist_unop
modified theorem Subtype.image_closedEBall
modified theorem Subtype.image_eball
modified theorem Subtype.preimage_eball
modified theorem uniformity_edist
added theorem MulOpposite.edist_op
added theorem MulOpposite.edist_unop