Theorem HolderOnWith.dist_le_of_le

Modification history

2024-12-23 08:45

Mathlib/Topology/MetricSpace/Holder.lean

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

Added HolderOnWith.dist_le_of_le View on Github →