Theorem HolderWith.restrict_iff

Modification history

2026-07-20 01:34

Mathlib/Topology/MetricSpace/Holder.lean

refactor: rename restrict to domRestrict (#25980) …

Modified HolderWith.restrict_iff View on Github →

2024-12-23 08:45

Mathlib/Topology/MetricSpace/Holder.lean

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

Added HolderWith.restrict_iff View on Github →