Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.subsingleton.holder_on_with

Modification history

2021-07-31 20:17

src/topology/metric_space/holder.lean

feat(topology/metric_space/holder): add `holder_on_with` (#8454)

Added set.subsingleton.holder_on_with View on Github →