Theorem PseudoMetric.finsetSup_apply

Modification history

2025-05-13 16:33
Mathlib/Topology/MetricSpace/BundledFun.lean
feat(Topology/MetricSpace): pseudometrics as bundled functions (#23111) …
Added PseudoMetric.finsetSup_applyView on Github →