mathlib3
bcd79a1f - chore(analysis/normed/group/basic): rename vars (#9652)

Commit
4 years ago
chore(analysis/normed/group/basic): rename vars (#9652) * use `E`, `F` for (semi)normed groups and greek letters for other types; * golf some proofs (`bounded_iff_forall_norm_le`, `norm_pos_iff'`); * use `namespace lipschitz_with` and `namespace antilipschitz_with` instead of manual prefixes for all lemmas; * generalize `antilipschitz_with.add_lipschitz_with` to `pseudo_emetric_space`; * add `antilipschitz_with.edist_lt_top` and `antilipschitz_with.edist_ne_top`; * fix a typo in `pseudo_emetric_space.to_pseudo_metric_space`.
Author
Parents
Loading