Commit 2024-12-23 08:45 f0ccda83

View on Github →

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

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Defs.lean

added theorem Subtype.edist_mk_mk

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

Modified Mathlib/Topology/MetricSpace/Holder.lean

added theorem HolderOnWith.dist_le

added theorem HolderOnWith.dist_le_of_le

added theorem HolderOnWith.nndist_le

added theorem HolderOnWith.nndist_le_of_le

added theorem HolderWith.restrict_iff