Theorem LipschitzWith.nnorm_le_mul'

Modification history

2024-06-20 19:07

Mathlib/Analysis/Normed/Group/Basic.lean

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

Modified LipschitzWith.nnorm_le_mul'View on Github →

2023-07-16 11:34

Mathlib/Analysis/Normed/Group/Basic.lean

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

Added LipschitzWith.nnorm_le_mul'View on Github →