Theorem MemHolder.of_le'

Modification history

2025-11-26 16:01
Mathlib/Topology/MetricSpace/HolderNorm.lean
feat: monotonicity of Holderianity (#31561) …
Added MemHolder.of_le'View on Github →