Theorem HolderWith.holderWith_zero_of_bounded

Modification history

2025-11-26 16:01
Mathlib/Topology/MetricSpace/Holder.lean
feat: monotonicity of Holderianity (#31561) …
Added HolderWith.holderWith_zero_of_boundedView on Github →