Commit 2025-05-13 16:33 f372074b

View on Github →

feat(Topology/MetricSpace): pseudometrics as bundled functions (#23111) Preparation for results using families of pseudometrics

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/BundledFun.lean

added theorem PseudoMetric.IsUltra.finsetSup

added theorem PseudoMetric.IsUltra.isTransitiveRel_ball

added theorem PseudoMetric.IsUltra.isTransitiveRel_closedBall

added theorem PseudoMetric.IsUltra.le_sup

added theorem PseudoMetric.coe_bot

added theorem PseudoMetric.coe_finsetSup

added theorem PseudoMetric.coe_mk

added theorem PseudoMetric.coe_sup

added theorem PseudoMetric.finsetSup_apply

added theorem PseudoMetric.isSymmetricRel_ball

added theorem PseudoMetric.isSymmetricRel_closedBall

added theorem PseudoMetric.mk_apply

added structure PseudoMetric