Commit 2021-10-11 04:03 bcd79a1f
View on Github →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
andnamespace antilipschitz_with
instead of manual prefixes for all lemmas; - generalize
antilipschitz_with.add_lipschitz_with
topseudo_emetric_space
; - add
antilipschitz_with.edist_lt_top
andantilipschitz_with.edist_ne_top
; - fix a typo in
pseudo_emetric_space.to_pseudo_metric_space
.