pi_Lp): generalize to pseudo_metric (#6978)

Commit

4 years ago

refactor(topology/metric_space/pi_Lp): generalize to pseudo_metric (#6978) We generalize here the Lp distance to `pseudo_emetric` and similar concepts.

Author

riccardobrasca

Parents

b7fbc17a

mathlib 64abe48e - refactor(topology/metric_space/pi_Lp): generalize to pseudo_metric (#6978)

mathlib
64abe48e - refactor(topology/metric_space/pi_Lp): generalize to pseudo_metric (#6978)