Theorem PseudoMetric.IsUltra.isTransitiveRel_ball

Modification history

2025-10-24 14:57
Mathlib/Topology/MetricSpace/BundledFun.lean
refactor(Topology/UniformSpace): use `SetRel` (#23181) …
Deleted PseudoMetric.IsUltra.isTransitiveRel_ballView on Github →
2025-05-13 16:33
Mathlib/Topology/MetricSpace/BundledFun.lean
feat(Topology/MetricSpace): pseudometrics as bundled functions (#23111) …
Added PseudoMetric.IsUltra.isTransitiveRel_ballView on Github →