Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`.
- Loading branch information