Theorem HolderOnWith.nndist_le

Modification history

2024-12-23 08:45

Mathlib/Topology/MetricSpace/Holder.lean

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

Added HolderOnWith.nndist_le View on Github →