Theorem Subtype.edist_mk_mk

Modification history

2024-12-23 08:45

Mathlib/Topology/EMetricSpace/Defs.lean

feat(Holder): generalize a section to `HolderOnWith` (#20164)

Added Subtype.edist_mk_mk View on Github →