mathlib3
60371b88 - refactor(topology/metric_space/lipschitz): use `function.End` (#14502)

Commit
3 years ago
refactor(topology/metric_space/lipschitz): use `function.End` (#14502) This way we avoid dependency on `category_theory`.
Author
Parents
Loading