Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-23 15:29 78034350

View on Github →

refactor(topology/metric_space/lipschitz): generalize to pseudo_emetric_space (#6831) This is part of a series of PR to introduce semi_normed_group in mathlib. We introduce here Lipschitz maps for pseudo_emetric_space (I also improve some theorem name in topology/metric_space/emetric_space).

Estimated changes

modified theorem edist_pi_const
modified theorem edist_pi_def
modified theorem prod.edist_eq
deleted theorem prod.pesudoedist_eq
deleted theorem pseudo_edist_pi_const
deleted theorem pseudo_edist_pi_def
modified theorem lipschitz_on_univ
modified theorem lipschitz_on_with.mono
modified def lipschitz_on_with
modified theorem lipschitz_on_with_empty
modified def lipschitz_with