Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-24 19:56 cdaa6d2b

View on Github →

refactor(analysis/normed_space/pi_Lp): golf some instances (#14339)

  • drop pi_Lp.emetric_aux;
  • use T₀ to get (e)metric_space from pseudo_(e)metric_space;
  • restate pi_Lp.(anti)lipschitz_with_equiv with correct pseudo_emetric_space instances; while they're defeq, it's better not to leak auxiliary instances unless necessary.

Estimated changes

modified theorem pi_Lp.edist_eq
deleted def pi_Lp.emetric_aux
modified theorem pi_Lp.lipschitz_with_equiv