Theorem AntilipschitzWith.le_mul_nnnorm'

Modification history

2024-06-20 19:07

Mathlib/Analysis/Normed/Group/Basic.lean

chore: move some lemmas to Analysis.Normed.Group.Uniform (#13945) …

Modified AntilipschitzWith.le_mul_nnnorm'View on Github →

2023-07-16 11:34

Mathlib/Analysis/Normed/Group/Basic.lean

chore: forward-port leanprover-community/mathlib#19103 (#5855)

Added AntilipschitzWith.le_mul_nnnorm'View on Github →